finrank_quotient_add_finrank — Mathlib

English

Let L be a submodule of M and f: M → N a linear map. If finrank L ≤ finrank (L mapped by f), then L ∩ ker f = {0}.

Русский

Пусть L — подмодуль M и f: M → N линейна. Если ранги удовлетворяют неравенству, то пересечение L и ker f тривиально.

LaTeX

$$$\operatorname{finrank}_R L \le \operatorname{finrank}_R(L\xrightarrow{f} N) \Rightarrow L \cap \ker f = \{0\}. $$$

Lean4

/-- Rank-nullity theorem using `finrank`. -/
theorem finrank_quotient_add_finrank [Module.Finite R M] (N : Submodule R M) :
    finrank R (M ⧸ N) + finrank R N = finrank R M :=
  by
  rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
    Submodule.finrank_eq_rank]
  exact HasRankNullity.rank_quotient_add_rank _

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