English
For finite K,V with a finite structure, the cardinal of V equals the cardinal of K raised to the rank, as in Module.card_eq_pow_finrank.
Русский
Для конечных K, V справедливо, что кардинал V равен кардиналу K, возведённому в ранк, как в Module.card_eq_pow_finrank.
LaTeX
$$$ \\mathrm{Nat.card} V = \\mathrm{Nat.card} K^{\\,\\mathrm{finrank} K V} $$$
Lean4
/-- A module over a division ring is Noetherian if and only if it is finitely generated. -/
theorem iff_fg : IsNoetherian K V ↔ Module.Finite K V :=
by
constructor
· intro h
exact
⟨⟨finsetBasisIndex K V, by
convert (finsetBasis K V).span_eq
simp⟩⟩
· rintro ⟨s, hs⟩
rw [IsNoetherian.iff_rank_lt_aleph0, ← rank_top, ← hs]
exact lt_of_le_of_lt (rank_span_le _) s.finite_toSet.lt_aleph0
