basisUnitLattice — Mathlib

English

A corresponding basis for the quotient (𝓞 K)ˣ/(torsion K) exists with card Fin (rank K).

Русский

Существуют базы для квоты (𝓞 K)ˣ/(torsion K) размером Fin(rank K).

LaTeX

$$basisModTorsion : Basis (Fin (NumberField.Units.rank K)) Int (Additive (HasQuotient.Quotient (Units (NumberField.RingOfIntegers K)) (NumberField.Units.torsion K)))$$

Lean4

/-- The basis of the `unitLattice` obtained by mapping `basisModTorsion` via `logEmbedding`. -/
def basisUnitLattice : Basis (Fin (rank K)) ℤ (unitLattice K) :=
  (basisModTorsion K).map (logEmbeddingEquiv K)

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