unitsComplexConj_torsion

Mathlib.NumberTheory.NumberField.CMField

URI: https://scilib.ai/kg/mathlib#NumberField.IsCMField.unitsComplexConj_torsion

English

For units u in the ring of integers, complexConj_K(u) = u iff u lies in realUnits(K).

Русский

Для единиц u из кольца целых, complexConj_K(u)=u тогда и только тогда, когда u лежит в realUnits(K).

LaTeX

$$$$ complexConj_K(u)=u \\iff u \\in \\mathrm{realUnits}(K). $$$$

Lean4

theorem unitsComplexConj_torsion (ζ : torsion K) : unitsComplexConj K ζ = ζ⁻¹ :=
  by
  apply coe_injective
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru