realUnits — Mathlib

English

The subgroup realUnits(K) is the subgroup of units generated by the units of K^+; equivalently, realUnits(K) is the range of Units.map from (𝓞K^+)^× to (𝓞K)^×.

Русский

Подгруппа realUnits(K) порождается единицами K^+; то есть это образ отображения Units.map от (𝓞K^+)^× в (𝓞K)^×.

LaTeX

$$$$ \\mathrm{realUnits}(K) = \\mathrm{range}\\bigl( \\mathrm{Units.map}\\bigl( \\iota: (\\\\mathcal{O}_{K^+})^{\\times} \\to (\\\\mathcal{O}_K)^{\\times} \\bigr) \\bigr) $$$$

Lean4

/-- The subgroup of `(𝓞 K)ˣ` generated by the units of `K⁺`. These units are exactly the units fixed
by the complex conjugation, see `IsCMField.unitsComplexConj_eq_self_iff`.
-/
def realUnits : Subgroup (𝓞 K)ˣ :=
  (Units.map (algebraMap (𝓞 K⁺) (𝓞 K)).toMonoidHom).range

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