logEmbeddingQuot_apply — Mathlib

English

The finite rank of the quotient by torsion equals the Dirichlet unit rank.

Русский

Число степеней свободы модуля делится на torsion и равно рангу единиц Дирихле.

LaTeX

$$Module.finrank(\mathbb{Z})( (\mathcal O_K)^{\times} / torsion(K) ) = rank(K)$$

Lean4

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

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