coe_natCast

Mathlib.NumberTheory.Padics.Complex

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

← MathLib Explorer

English

The natural numbers embed compatibly into ℂ_p via PadicAlgCl(p).

Русский

Натуральные числа естественным образом внедряются в ℂ_p через PadicAlgCl(p).

LaTeX

$$$((n : \mathrm{PadicAlgCl}(p)) : \mathbb{C}_p) = (n : \mathbb{C}_p).$$$

Lean4

@[simp, norm_cast]
theorem coe_natCast (n : ℕ) : ((n : PadicAlgCl p) : ℂ_[p]) = (n : ℂ_[p]) := by
  rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]) n, coe_eq]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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