completeBasis_apply_of_ne — Mathlib

English

For i, expMap (completeBasis i) equals the global norm map at all places for the corresponding fundSystem element.

Русский

Для i: expMap(completeBasis(i)) = normAtAllPlaces(mixedEmbedding(fundSystem(i))).

LaTeX

$$$\expMap(\text{completeBasis}(i)) = \mathrm{normAtAllPlaces}(\mathrm{mixedEmbedding}(K)(\mathrm{fundSystem}(K)(\operatorname{equivFinRank}(i))))$$$

Lean4

theorem completeBasis_apply_of_ne (i : { w : InfinitePlace K // w ≠ w₀ }) :
    completeBasis K i = expMap.symm (normAtAllPlaces (mixedEmbedding K (fundSystem K (equivFinRank.symm i)))) := by
  rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_neg]

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