English
If emultiplicity p a ≠ emultiplicity p b, then emultiplicity p (a + b) equals the minimum of emultiplicity p a and emultiplicity p b.
Русский
Если эмптимпликативность p a не равна emultiplicity p b, то emultiplicity p (a + b) равно минимуму между emultiplicity p a и emultiplicity p b.
LaTeX
$$$ \forall {\alpha} [Ring \alpha] {p a b}, Ne (emultiplicity p a) (emultiplicity p b) \to emultiplicity p (a+b) = \min\big( emultiplicity p a, emultiplicity p b \big) $$$
Lean4
theorem emultiplicity_add_eq_min {p a b : α} (h : emultiplicity p a ≠ emultiplicity p b) :
emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b) :=
by
rcases lt_trichotomy (emultiplicity p a) (emultiplicity p b) with (hab | _ | hab)
· rw [add_comm, emultiplicity_add_of_gt hab, min_eq_left]
exact le_of_lt hab
· contradiction
· rw [emultiplicity_add_of_gt hab, min_eq_right]
exact le_of_lt hab
