English
Two positive integers are equal if and only if all their p-adic valuations agree for every prime p (under the nonzero hypothesis).
Русский
Два положительных числа равны тогда и только тогда, когда для каждого простого p их p-адические порядки совпадают (при условии не нуля).
LaTeX
$$$ a = b \iff \forall p. p \ text{ Prime } \rightarrow padicValNat p a = padicValNat p b $ (for $a,b\neq 0$)$$
Lean4
/-- Two positive naturals are equal if their prime padic valuations are equal -/
theorem eq_iff_prime_padicValNat_eq (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :
a = b ↔ ∀ p : ℕ, p.Prime → padicValNat p a = padicValNat p b :=
by
constructor
· rintro rfl
simp
· intro h
refine eq_of_factorization_eq ha hb fun p => ?_
by_cases pp : p.Prime
· simp [factorization_def, pp, h p pp]
· simp [factorization_eq_zero_of_non_prime, pp]
