finrank_range_add_finrank_ker — Mathlib

English

Rank-nullity theorem: the sum of finrank of the range and the kernel of a linear map equals finrank of the domain.

Русский

Теорема о ранге и нулевой области: сумма финранка образа и нуля равна фінранку пространства источника.

LaTeX

$$[FiniteDimensional K V] (f : V →ₗ[K] V₂) : finrank K (LinearMap.range f) + finrank K (LinearMap.ker f) = finrank K V$$

Lean4

/-- rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to
the dimension of the source space. -/
theorem finrank_range_add_finrank_ker [FiniteDimensional K V] (f : V →ₗ[K] V₂) :
    finrank K (LinearMap.range f) + finrank K (LinearMap.ker f) = finrank K V :=
  by
  rw [← f.quotKerEquivRange.finrank_eq]
  exact Submodule.finrank_quotient_add_finrank _

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