unitsComplexConj_eq_self_iff — Mathlib

English

For x in 𝓞K, complexConj_K(x) = x if and only if there exists y in 𝓞K^+ with algebraMap(y) = x.

Русский

Для x в 𝓞K, complexConj_K(x) = x тогда и только тогда, когда существует y в 𝓞K^+ с algebraMap(y)=x.

LaTeX

$$$$ complexConj_K(x)=x \\iff \\\\exists y \in \mathcal{O}_{K^+}, \\\\mathrm{algebraMap}_{\\\\mathcal{O}_{K^+} \\to \\\\mathcal{O}_K}(y)=x. $$$$

Lean4

theorem unitsComplexConj_eq_self_iff (u : (𝓞 K)ˣ) : unitsComplexConj K u = u ↔ u ∈ realUnits K := by
  simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv, AlgEquiv.toRingEquiv_eq_coe,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply, AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) K]

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