coe_add

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The inclusion map from the p-adic integers to the p-adic numbers preserves addition: the image of z1+z2 equals the sum of the images.

Русский

Включение ℤ_p в ℚ_p сохраняет сложение: образ z1+z2 равен сумме образов z1 и z2.

LaTeX

$$$((z_1+z_2 : \mathbb{Z}_p) : \mathbb{Q}_p) = z_1 + z_2$$$

Lean4

@[simp, norm_cast]
theorem coe_add (z1 z2 : ℤ_[p]) : ((z1 + z2 : ℤ_[p]) : ℚ_[p]) = z1 + z2 :=
  rfl

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

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

Разделы

Аффилиация

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