English
Let p, a, b be elements of a ring α. If the p-adic emultiplicity of b is strictly smaller than that of a, then the emultiplicity of a + b equals the emultiplicity of b.
Русский
Пусть p, a, b — элементы кольца α. Если p-расширенная кратность b строго меньше p-расширенной кратности a, то кратность p суммы a + b равна кратности p b.
LaTeX
$$$ \forall p,a,b \in \alpha, emultiplicity p b < emultiplicity p a \Rightarrow emultiplicity p (a+b) = emultiplicity p b $$$
Lean4
theorem emultiplicity_add_of_gt {p a b : α} (h : emultiplicity p b < emultiplicity p a) :
emultiplicity p (a + b) = emultiplicity p b :=
by
have : FiniteMultiplicity p b := finiteMultiplicity_iff_emultiplicity_ne_top.2 (by simp [·] at h)
rw [this.emultiplicity_eq_multiplicity] at *
apply emultiplicity_eq_of_dvd_of_not_dvd
· apply dvd_add
· apply pow_dvd_of_le_emultiplicity
exact h.le
· simp
· rw [dvd_add_right]
· apply this.not_pow_dvd_of_multiplicity_lt
simp
apply pow_dvd_of_le_emultiplicity
exact Order.add_one_le_of_lt h
