English
If p ≠ 1, multiplicity p a ≤ multiplicity p b, and a and b are coprime, then multiplicity p a = 0.
Русский
Если p ≠ 1, и кратность p a ≤ кратности p b, а a и b — coprime, то кратность p a равна 0.
LaTeX
$$$ hp \neq 1 \to multiplicity p a \le multiplicity p b \to a \text{ и } b \coprime \Rightarrow multiplicity p a = 0 $$$
Lean4
theorem multiplicity_eq_zero_of_coprime {p a b : ℕ} (hp : p ≠ 1) (hle : multiplicity p a ≤ multiplicity p b)
(hab : Nat.Coprime a b) : multiplicity p a = 0 :=
by
apply Nat.eq_zero_of_not_pos
intro nh
have da : p ∣ a := by simpa [multiplicity_eq_zero] using nh.ne.symm
have db : p ∣ b := by simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm
have := Nat.dvd_gcd da db
rw [Coprime.gcd_eq_one hab, Nat.dvd_one] at this
exact hp this
