norm_natCast_zmodRepr_eq_one_iff_ne

English

The norm relation equivalences give a zero/one dichotomy: either ∥(x.zmodRepr)∥ = 1 or x = 0.

Русский

Норма даёт двойственную зависимость: либо ∥(x.zmodRepr)∥ = 1, либо x = 0.

LaTeX

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

Lean4

theorem norm_natCast_zmodRepr_eq_one_iff_ne (x : ℤ_[p]) : ‖(x.zmodRepr : ℤ_[p])‖ = 1 ↔ x.zmodRepr ≠ 0 :=
  by
  rw [norm_natCast_zmodRepr_eq_one_iff, ne_eq, zmodRepr_eq_zero_iff_dvd, ← norm_lt_one_iff_dvd]
  simp

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