coe_eq_algebraMap

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.coe_eq_algebraMap

English

For every x in 𝓞K, the underlying element in K equals the image of x under the structure map algebraMap.

Русский

Для каждого x ∈ 𝓞K подлежащий элемент в K равен образу x под маппингом algebraMap.

LaTeX

$$$(x:K) = \\mathrm{algebraMap}_{\\mathcal{O}_K,K} x$$

Lean4

theorem coe_eq_algebraMap (x : 𝓞 K) : (x : K) = algebraMap _ _ x :=
  rfl

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

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

Разделы

Аффилиация

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