padic_norm_e_of_padicInt

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The norm is compatible with the p-adic rational embedding: for z in Z_p, the p-adic norm equals the norm from Q_p.

Русский

Согласование нормы: для z ∈ Z_p нормa p-адических чисел равна норме, полученной через вложение в Q_p.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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