Prove2Me

Dimension of a quotient space

Proved
WorkbookRestored.plus_45791

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For a real vector space XX and a subspace YY, dim⁡Y+dim⁡(X/Y)=dim⁡X\dim Y+\dim(X/Y)=\dim X. Dimensions are cardinal ranks, so the statement covers infinite-dimensional spaces as well.

Source: Lean-Workbook row lean_workbook_plus_45791 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.LinearAlgebra.Dimension.DivisionRing
Formal statement
theorem WorkbookRestored.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/blob/main/lean_workbook.json, row lean_workbook_plus_45791; immutable original Prove2Me node 8923a231-b5d6-458c-b554-cd99e810629c

View graph