English
If p is prime and hfin: FiniteMultiplicity p (a·b), then multiplicity p (a·b) = multiplicity p a + multiplicity p b.
Русский
Пусть p — простое, и FiniteMultiplicity p (a·b); тогда кратность p (a·b) равна сумме кратностей p a и p b.
LaTeX
$$$ \forall {a,b}, (hfin : FiniteMultiplicity p (a b)) \Rightarrow multiplicity p (a b) = multiplicity p a + multiplicity p b $$$
Lean4
theorem multiplicity_mul {p a b : α} (hp : Prime p) (hfin : FiniteMultiplicity p (a * b)) :
multiplicity p (a * b) = multiplicity p a + multiplicity p b :=
by
have hdiva : p ^ multiplicity p a ∣ a := pow_multiplicity_dvd ..
have hdivb : p ^ multiplicity p b ∣ b := pow_multiplicity_dvd ..
have hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b := by rw [pow_add]; gcongr
have hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b := fun h =>
not_or_intro (hfin.mul_left.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
(hfin.mul_right.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
(_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)
rw [hfin.multiplicity_eq_iff]
exact ⟨hdiv, hsucc⟩
