rank' — Mathlib

English

Any lattice has R-rank equal to the K-rank of V, under the fractional ring conditions.

Русский

Любая решётка имеет равный ранг по R и ранг по K в V (при условиях дробного кольца).

LaTeX

$$$ IsLattice\_rank' $$$

Lean4

/-- Any lattice has `R`-rank equal to the `K`-rank of `V`. -/
theorem rank' [IsFractionRing R K] (M : Submodule R V) [IsLattice K M] : Module.rank R M = Module.rank K V :=
  by
  let b := Module.Free.chooseBasis R M
  rw [rank_eq_card_basis b, ← rank_eq_card_basis (b.extendOfIsLattice K)]

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