ringOfIntegersComplexConj — Mathlib

English

There is a canonical algebra equivalence on the ring of integers given by complex conjugation, reflecting the CM-structure.

Русский

Существует каноническое эквивалентное отображение на кольце целых чисел, задаваемое конъюгированием, отражающее структуру CM-поля.

LaTeX

$$$\\mathcal{O}_K \\simeq_{\\mathcal{O}_{K^+}} \\mathcal{O}_K$$$

Lean4

/-- A variant of the complex conjugation defined as an `AlgEquiv` on the ring of integers.
-/
noncomputable abbrev ringOfIntegersComplexConj : (𝓞 K) ≃ₐ[𝓞 K⁺] (𝓞 K) :=
  RingOfIntegers.mapAlgEquiv (complexConj K)

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