expMap_basis_of_eq — Mathlib

English

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

Русский

Для i ≠ w0: expMap(completeBasis i) = normAtAllPlaces(mixedEmbedding(K, fundSystem(... i))).

LaTeX

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

Lean4

theorem expMap_basis_of_eq : expMap (completeBasis K w₀) = fun _ ↦ Real.exp 1 :=
  by
  ext
  simp_rw [expMap_apply, completeBasis_apply_of_eq, inv_mul_cancel₀ mult_coe_ne_zero]

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