norm_natCast_p_sub_one

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The norm of p−1 is 1 in Z_p.

Русский

Норма p−1 равна 1 в Z_p.

LaTeX

$$$$\|p-1\| = 1.$$$$

Lean4

@[simp]
theorem norm_natCast_p_sub_one : ‖((p - 1 : ℕ) : ℤ_[p])‖ = 1 := by simp [norm_def]

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

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

Разделы

Аффилиация

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