completeBasis — Mathlib

English

For i with i ≠ w0, completeBasis K i equals expMap.symm (normAtAllPlaces (mixedEmbedding K (fundSystem K (equivFinRank.symm i))))

Русский

Для i ≠ w0, completeBasis K i равно expMap.symm (normAtAllPlaces (mixedEmbedding K (fundSystem K (equivFinRank.symm i))))

LaTeX

$$$completeBasis(K,i) = \expMap^{-1}(\mathrm{normAtAllPlaces}(\mathrm{mixedEmbedding}(K)(\mathrm{fundSystem}(K)(\operatorname{equivFinRank}(i)^{ -1}))))$ for i ≠ w0$$

Lean4

/-- A basis of `realSpace K` formed by the image of the fundamental units
(which form a basis of a subspace `{x : realSpace K | ∑ w, x w = 0}`) and the vector `(mult w)_w`.
For `i ≠ w₀`, the image of `completeBasis K i` by the natural restriction map
`realSpace K → logSpace K` is `basisUnitLattice K`
-/
def completeBasis : Basis (InfinitePlace K) ℝ (realSpace K) :=
  basisOfLinearIndependentOfCardEqFinrank (linearIndependent_completeFamily K)
    (Module.finrank_fintype_fun_eq_card _).symm

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