English
For prime p, emultiplicity p (a · b) = emultiplicity p a + emultiplicity p b.
Русский
Для простого p эмптимпликативность (а · b) равна сумме эмптимпликативностей a и b.
LaTeX
$$$ emultiplicity p (a b) = emultiplicity p a + emultiplicity p b $$$
Lean4
theorem emultiplicity_mul {p a b : α} (hp : Prime p) :
emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b :=
by
by_cases hfin : FiniteMultiplicity p (a * b)
· rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
hfin.mul_right.emultiplicity_eq_multiplicity]
norm_cast
exact multiplicity_mul hp hfin
· rw [emultiplicity_eq_top.2 hfin, eq_comm, WithTop.add_eq_top, emultiplicity_eq_top, emultiplicity_eq_top]
simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin
