English
Let p, a, b be elements of α, with FiniteMultiplicity p b and multiplicity p b < multiplicity p a. Then multiplicity p (a + b) = multiplicity p b.
Русский
Пусть p, a, b — элементы кольца α; если FiniteMultiplicity p b и кратность p b меньше кратности p a, то кратность p суммы a + b равна кратности p b.
LaTeX
$$$ \forall p,a,b \in \alpha, FiniteMultiplicity p b \to multiplicity p b < multiplicity p a \to multiplicity p (a+b) = multiplicity p b $$$
Lean4
theorem multiplicity_add_of_gt {p a b : α} (hf : FiniteMultiplicity p b) (h : multiplicity p b < multiplicity p a) :
multiplicity p (a + b) = multiplicity p b :=
multiplicity_eq_of_emultiplicity_eq <|
emultiplicity_add_of_gt
(hf.emultiplicity_eq_multiplicity ▸ (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity)
