coe_eq

Mathlib.NumberTheory.Padics.Complex

URI: https://scilib.ai/kg/mathlib#PadicComplex.coe_eq

English

For any x in PadicAlgCl(p), its image in ℂ_p equals the algebra map applied to x.

Русский

Любой элемент x из PadicAlgCl(p) отображается в ℂ_p как алгебраическая карта x.

LaTeX

$$$(x : \mathbb{C}_p) = \operatorname{algebraMap}_{\mathrm{PadicAlgCl}(p) \to \mathbb{C}_p}(x).$$$

Lean4

theorem coe_eq (x : PadicAlgCl p) : (x : ℂ_[p]) = algebraMap (PadicAlgCl p) ℂ_[p] x :=
  rfl

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

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

Разделы

Аффилиация

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