eq_ratNorm

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#Padic.eq_ratNorm

English

For every p-adic q, the norm ‖q‖ equals the rational ratNorm(q).

Русский

Для каждого p-адического числа q нормa ‖q‖ равна рациональному ratNorm(q).

LaTeX

$$$\\|q\\| = \\operatorname{ratNorm}(q)$.$$

Lean4

theorem eq_ratNorm (q : ℚ_[p]) : ‖q‖ = ratNorm q :=
  Classical.choose_spec (padicNormE.is_rat q)

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

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

Разделы

Аффилиация

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