rank_range_add_rank_ker — Mathlib

English

Under base change bc, the finite rank of P over T equals the finite rank of M over R: finrank_T P = finrank_R M.

Русский

При базовом изменении bc имеет место равенство конечных рангов: finrank_T P = finrank_R M.

LaTeX

$$$\operatorname{finrank} T P = \operatorname{finrank} R M$$$

Lean4

/-- The **rank-nullity theorem** -/
theorem rank_range_add_rank_ker (f : M →ₗ[R] M₁) :
    Module.rank R (LinearMap.range f) + Module.rank R (LinearMap.ker f) = Module.rank R M :=
  by
  haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)
  rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]

Похожие утверждения