English
For a prime p in a CancelCommMonoidWithZero α, for all n,m ∈ ℕ, if p^{n+1} ∤ a and p^{m+1} ∤ b, then p^{n+m+1} ∤ a·b.
Русский
Пусть p — простое число в CancelCommMonoidWithZero α. Тогда для всех n,m ∈ ℕ, если p^{n+1} не делит a и p^{m+1} не делит b, то p^{n+m+1} не делит a·b.
LaTeX
$$$ \forall {n,m : \mathbb{N}}, \; p^{(n+1)} \nmid a \; \to \; p^{(m+1)} \nmid b \; \to \; p^{(n+m+1)} \nmid a b $$$
Lean4
theorem finiteMultiplicity_mul_aux {p : α} (hp : Prime p) {a b : α} :
∀ {n m : ℕ}, ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b
| n, m => fun ha hb ⟨s, hs⟩ =>
have : p ∣ a * b := ⟨p ^ (n + m) * s, by simp [hs, pow_add, mul_comm, mul_left_comm]⟩
(hp.2.2 a b this).elim
(fun ⟨x, hx⟩ =>
have hn0 : 0 < n := Nat.pos_of_ne_zero fun hn0 => by simp [hx, hn0] at ha
have hpx : ¬p ^ (n - 1 + 1) ∣ x := fun ⟨y, hy⟩ =>
ha
(hx.symm ▸
⟨y,
mul_right_cancel₀ hp.1 <|
by
rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy
simp [hy, pow_add, mul_comm, mul_left_comm]⟩)
have : 1 ≤ n + m := le_trans hn0 (Nat.le_add_right n m)
finiteMultiplicity_mul_aux hp hpx hb
⟨s,
mul_right_cancel₀ hp.1
(by
rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]
simp_all [mul_comm, mul_left_comm, pow_add])⟩)
fun ⟨x, hx⟩ =>
have hm0 : 0 < m := Nat.pos_of_ne_zero fun hm0 => by simp [hx, hm0] at hb
have hpx : ¬p ^ (m - 1 + 1) ∣ x := fun ⟨y, hy⟩ =>
hb
(hx.symm ▸
⟨y,
mul_right_cancel₀ hp.1 <| by
rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy
simp [hy, pow_add, mul_comm, mul_left_comm]⟩)
finiteMultiplicity_mul_aux hp ha hpx
⟨s,
mul_right_cancel₀ hp.1
(by
rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]
simp_all [mul_comm, mul_left_comm, pow_add])⟩
