basisModTorsion — Mathlib

English

A basis for unitLattice is obtained by mapping basisModTorsion through logEmbeddingEquiv.

Русский

База для unitLattice получается из образа basisModTorsion через logEmbeddingEquiv.

LaTeX

$$basisUnitLattice : Basis (Fin (rank K)) \mathbb{Z} (unitLattice K) = (basisModTorsion K).map (logEmbeddingEquiv K)$$

Lean4

/-- A basis of the quotient `(𝓞 K)ˣ ⧸ (torsion K)` seen as an additive ℤ-module. -/
def basisModTorsion : Basis (Fin (rank K)) ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
  Basis.reindex (Module.Free.chooseBasis ℤ _)
    (Fintype.equivOfCardEq <| by rw [← Module.finrank_eq_card_chooseBasisIndex, rank_modTorsion, Fintype.card_fin])

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