coe_mul

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The coercion from ℤ_p to ℚ_p preserves multiplication: the image of z1*z2 equals the product of the images.

Русский

Коэрцирование из ℤ_p в ℚ_p сохраняет умножение: образ z1 z2 равен произведению образов.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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