fg_iff_spanRank_eq_spanFinrank — Mathlib

English

A submodule is finitely generated if and only if its spanRank equals its spanFinrank (with the appropriate Cast).

Русский

Подпространение конечнопорождено ⇔ spanRank(p) = spanFinrank(p).

LaTeX

$$$p.spanRank = p.spanFinrank.cast \iff p.FG$$$

Lean4

/-- A submodule is finitely generated if and only if its `spanRank` is equal to its `spanFinrank`.
-/
theorem fg_iff_spanRank_eq_spanFinrank {p : Submodule R M} : p.spanRank = p.spanFinrank ↔ p.FG :=
  by
  rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm]
  exact cast_toNat_eq_iff_lt_aleph0

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