norm_intCast_eq_padic_norm

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

For any integer z, the norm of its image in Z_p equals the norm of its image in Q_p.

Русский

Для любого целого z норма образа z в Z_p равна норме образа z в Q_p.

LaTeX

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

Lean4

theorem norm_intCast_eq_padic_norm (z : ℤ) : ‖(z : ℤ_[p])‖ = ‖(z : ℚ_[p])‖ := by simp [norm_def]

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

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

Разделы

Аффилиация

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