English
Let a be irreducible and b ≠ 0. Then for any natural number n, ↑n ≤ emultiplicity a b if and only if replicate n (normalize a) ≤ normalizedFactors b.
Русский
Пусть a неразложимо и b ≠ 0. Тогда для любого натурального числа n выполнено: ↑n ≤ emultiplicity a b тогда и только если replicate n (normalize a) ≤ normalizedFactors b.
LaTeX
$$$\uparrow n \le emultiplicity\ a\ b \iff replicate\ n\ (\normalize a) \le normalizedFactors\ b$$$
Lean4
theorem le_emultiplicity_iff_replicate_le_normalizedFactors {a b : R} {n : ℕ} (ha : Irreducible a) (hb : b ≠ 0) :
↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b :=
by
rw [← pow_dvd_iff_le_emultiplicity]
revert b
induction n with
| zero => simp
| succ n ih => ?_
intro b hb
constructor
· rintro ⟨c, rfl⟩
rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb
rw [pow_succ', mul_assoc, normalizedFactors_mul hb.1 hb.2, replicate_succ, normalizedFactors_irreducible ha,
singleton_add, cons_le_cons_iff, ← ih hb.2]
apply Dvd.intro _ rfl
· rw [Multiset.le_iff_exists_add]
rintro ⟨u, hu⟩
rw [← (prod_normalizedFactors hb).dvd_iff_dvd_right, hu, prod_add, prod_replicate]
exact (Associated.pow_pow <| associated_normalize a).dvd.trans (Dvd.intro u.prod rfl)
