one_le_norm_iff

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

For each x in Z_p, 1 ≤ ||x|| iff ||x|| = 1, capturing that the norm is at least 1 only when it equals 1.

Русский

Для каждого x ∈ Z_p, 1 ≤ ||x|| эквивалентно ||x|| = 1; норма либо меньше 1, либо равна 1.

LaTeX

$$$$1 \le \|x\| \;\Leftrightarrow\; \|x\| = 1.$$$$

Lean4

@[simp]
theorem one_le_norm_iff {x : ℤ_[p]} : 1 ≤ ‖x‖ ↔ ‖x‖ = 1 := by simp [le_antisymm_iff, ← padic_norm_e_of_padicInt, x.prop]

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

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

Разделы

Аффилиация

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