norm_natCast_zmodRepr_eq

Mathlib.NumberTheory.Padics.RingHoms

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

English

The norm equality ∥(x.zmodRepr)∥ = ∥x∥ is equivalent to ∥x∥ = 1 or x = 0.

Русский

Равенство норм ∥(x.zmodRepr)∥ = ∥x∥ эквивалентно ∥x∥ = 1 или x = 0.

LaTeX

$$∥(x.zmodRepr)∥ = ∥x∥ ↔ ∥x∥ = 1 ∨ x = 0$$

Lean4

theorem norm_natCast_zmodRepr_eq (x : ℤ_[p]) : ‖(x.zmodRepr : ℤ_[p])‖ = 1 ∨ x.zmodRepr = 0 := by
  grind [norm_natCast_zmodRepr_eq_one_iff_ne]

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

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

Разделы

Аффилиация

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