lean_workbook_plus_45791

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $Y$ be a subspace of $X$ , then prove that $dim(Y)+dim(X/Y)=dim(X)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45791 (X : Type*) [AddCommGroup X] [Module ℝ X]
    (Y : Submodule ℝ X) : Module.rank ℝ Y + Module.rank ℝ (X ⧸ Y) = Module.rank ℝ X   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph