generators_ncard — Mathlib

English

If p is finitely generated, then the generating set p.generators has cardinality equal to spanFinrank(p).

Русский

Если p конечно порождается, то множество порождающих p.generators имеет кардинал, равный spanFinrank(p).

LaTeX

$$$(\mathrm{generators}(p)).\mathrm{ncard} = \operatorname{spanFinrank}(p).$$$

Lean4

theorem generators_ncard {p : Submodule R M} (h : p.FG) : (generators p).ncard = spanFinrank p :=
  by
  rw [← Nat.cast_inj (R := Cardinal), ← fg_iff_spanRank_eq_spanFinrank.mpr h, Set.ncard, Set.encard, ENat.card,
    generators_card, toNat_toENat, ← spanFinrank]
  exact (fg_iff_spanRank_eq_spanFinrank.mpr h).symm

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