English
The p-adic norm of an integer m is 1 if and only if p does not divide m.
Русский
p-адическая норма целого числа m равна 1 тогда и только тогда, когда p не делит m.
LaTeX
$$$ padicNorm\ p\ m = 1 \iff \neg (p \mid m) $$$
Lean4
/-- The `p`-adic norm of an integer `m` is one iff `p` doesn't divide `m`. -/
theorem int_eq_one_iff (m : ℤ) : padicNorm p m = 1 ↔ ¬(p : ℤ) ∣ m :=
by
nth_rw 2 [← pow_one p]
simp only [dvd_iff_norm_le, Nat.cast_one, zpow_neg, zpow_one, not_le]
constructor
· intro h
rw [h, inv_lt_one₀] <;> norm_cast
· exact Nat.Prime.one_lt Fact.out
· exact Nat.Prime.pos Fact.out
· simp only [padicNorm]
split_ifs
· rw [inv_lt_zero, ← Nat.cast_zero, Nat.cast_lt]
intro h
exact (Nat.not_lt_zero p h).elim
· have : 1 < (p : ℚ) := by norm_cast; exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)
rw [← zpow_neg_one, zpow_lt_zpow_iff_right₀ this]
have : 0 ≤ padicValRat p m := by simp only [of_int, Nat.cast_nonneg]
intro h
rw [← zpow_zero (p : ℚ), zpow_right_inj₀] <;> linarith
