unitsComplexConj — Mathlib

English

Complex conjugation induces an isomorphism on the group of units of the ring of integers, i.e., unitsComplexConj_K: (𝓞K)ˣ ≃* (𝓞K)ˣ.

Русский

Комплексное сопряжение индуцирует изоморфизм на группе единиц кольца целых: unitsComplexConj_K: (𝓞K)ˣ ≃* (𝓞K)ˣ.

LaTeX

$$$$ units\\_conj_K: (\\\\mathcal{O}_K)^{\\times} \\cong (\\\\mathcal{O}_K)^{\\times} $$$$

Lean4

/-- The complex conjugation as an isomorphism of the units of `K`. -/
noncomputable abbrev unitsComplexConj : (𝓞 K)ˣ ≃* (𝓞 K)ˣ :=
  Units.mapEquiv <| RingOfIntegers.mapRingEquiv (complexConj K).toRingEquiv

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