completeBasis_apply_of_eq — Mathlib

English

The equality expMap (completeBasis i) = normAtAllPlaces (mixedEmbedding (fundSystem ... i)) holds whenever i ≠ w0, relating the exponential map image of the basis to the global norm map.

Русский

Справедливо равенство expMap(completeBasis i) = normAtAllPlaces(mixedEmbedding(... i)) для i ≠ w0.

LaTeX

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

Lean4

theorem completeBasis_apply_of_eq : completeBasis K w₀ = fun w ↦ (mult w : ℝ) := by
  rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_pos rfl]

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