finrank_of_pi — Mathlib

English

For M a submodule of ι → K that is an IsLattice over K, the finite rank over R equals card ι.

Русский

Для M как подмодуля ι → K, являющегося IsLattice над K, конечный ранг над R равен ι.

LaTeX

$$$\operatorname{finrank}_R M = |ι|$$$

Lean4

/-- `Module.finrank` version of `IsLattice.rank`. -/
theorem finrank_of_pi {ι : Type*} [Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K)) [IsLattice K M] :
    Module.finrank R M = Fintype.card ι :=
  Module.finrank_eq_of_rank_eq (IsLattice.rank_of_pi K M)

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