nat_eq_one_iff — Mathlib

English

The p-adic norm of a natural m is 1 if and only if p does not divide m.

Русский

Нормa p-адическая натурального m равна 1 тогда и только тогда, когда p не делит m.

LaTeX

$$$ padicNorm\ p\ m = 1 \iff \neg p \mid m $$$

Lean4

/-- The `p`-adic norm of a natural `m` is one iff `p` doesn't divide `m`. -/
theorem nat_eq_one_iff (m : ℕ) : padicNorm p m = 1 ↔ ¬p ∣ m := by
  rw [← Int.natCast_dvd_natCast, ← int_eq_one_iff, Int.cast_natCast]

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