coe_ringOfIntegersComplexConj

Mathlib.NumberTheory.NumberField.CMField

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

English

The inclusion of 𝓞K^+ into 𝓞K commutes with complex conjugation on representatives: (ringOfIntegersConj x) = complexConj x.

Русский

Включение 𝓞K^+ в 𝓞K commute с сопряжением: (ringOfIntegersConj_K)(x) = complexConj_K(x).

LaTeX

$$$$(ringOfIntegersConj_K\\, x : K) = \\mathrm{complexConj}_K(x)$$$$

Lean4

@[simp]
theorem coe_ringOfIntegersComplexConj (x : 𝓞 K) : (ringOfIntegersComplexConj K x : K) = complexConj K x :=
  rfl

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

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

Разделы

Аффилиация

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