rank_of_pi — Mathlib

English

Any R-lattice inside ι → K has R-rank equal to the cardinality of ι over K.

Русский

Каждая R-решётка в ι → K имеет ранг R, равный кардиналу множества ι.

LaTeX

$$$\operatorname{rank}_R M = |\iota|$$$

Lean4

/-- Any `R`-lattice in `ι → K` has `#ι` as `R`-rank. -/
theorem rank_of_pi {ι : Type*} [Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K)) [IsLattice K M] :
    Module.rank R M = Fintype.card ι := by
  rw [IsLattice.rank' K M]
  simp

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