logEmbeddingEquiv_apply — Mathlib

English

The logEmbeddingEquiv provides a linear equivalence between quotient units and the unit lattice.

Русский

logEmbeddingEquiv задаёт линейное эквивалентство между фактор-группой единиц и единичным решетом.

LaTeX

$$$\logEmbeddingEquiv K : ((\mathcal O_K)^{\times})/(torsion K) \simeq_{\mathbb{Z}} unitLattice(K)$$$

Lean4

@[simp]
theorem logEmbeddingEquiv_apply (x : (𝓞 K)ˣ) :
    logEmbeddingEquiv K (Additive.ofMul (QuotientGroup.mk x)) = logEmbedding K (Additive.ofMul x) :=
  rfl

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