English
If FiniteMultiplicity p a, FiniteMultiplicity p b, and multiplicity p a ≠ multiplicity p b, then multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b).
Русский
Если FiniteMultiplicity p a, FiniteMultiplicity p b, и multiplicity p a ≠ multiplicity p b, то multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b).
LaTeX
$$$ \forall {\alpha} [Ring α], ha : FiniteMultiplicity p a, hb : FiniteMultiplicity p b, h : multiplicity p a \neq multiplicity p b \Rightarrow multiplicity p (a+b) = \min\big( multiplicity p a, multiplicity p b \big)$$$
Lean4
theorem multiplicity_add_eq_min {p a b : α} (ha : FiniteMultiplicity p a) (hb : FiniteMultiplicity p b)
(h : multiplicity p a ≠ multiplicity p b) : multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b) :=
by
rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | _ | hab)
· rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]
exact le_of_lt hab
· contradiction
· rw [hb.multiplicity_add_of_gt hab, min_eq_right]
exact le_of_lt hab
