coe_intCast

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.coe_intCast

English

The integer z embedded into ℤ_p and then into ℚ_p equals z as a rational.

Русский

Целое z, встроенное в ℤ_p, затем в ℚ_p, равно z как рациональное число.

LaTeX

$$$((z : \mathbb{Z}_p) : \mathbb{Q}_p) = z$$$

Lean4

@[simp, norm_cast]
theorem coe_intCast (z : ℤ) : ((z : ℤ_[p]) : ℚ_[p]) = z :=
  rfl

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

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

Разделы

Аффилиация

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