English
Let p ∈ α, a, b ∈ α, with multiplicity p b < multiplicity p a and FiniteMultiplicity p b. Then multiplicity p (a − b) = multiplicity p b.
Русский
Пусть p ∈ α, элементы a, b ∈ α таковы, что multiplicity p b < multiplicity p a и FiniteMultiplicity p b. Тогда multiplicity p (a − b) = multiplicity p b.
LaTeX
$$$ \forall p,a,b \in \alpha, multiplicity p b < multiplicity p a \to FiniteMultiplicity p b \to multiplicity p (a-b) = multiplicity p b $$$
Lean4
theorem multiplicity_sub_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a) (hfin : FiniteMultiplicity p b) :
multiplicity p (a - b) = multiplicity p b := by
rw [sub_eq_add_neg, hfin.neg.multiplicity_add_of_gt] <;> rw [multiplicity_neg]; assumption
