English
For any a,b,c,d, emultiplicity a b ≤ emultiplicity c d if and only if for all n ∈ ℕ, a^n ∣ b implies c^n ∣ d.
Русский
Для любых a,b,c,d верно: emultiplicity a b ≤ emultiplicity c d тогда и только тогда, когда для всех n ∈ ℕ, если a^n ∣ b, то c^n ∣ d.
LaTeX
$$$ \forall n \in \mathbb{N},\ a^n \mid b \Rightarrow c^n \mid d \quad\iff\quad \operatorname{emultiplicity}(a,b) \le \operatorname{emultiplicity}(c,d)$$$
Lean4
theorem emultiplicity_le_emultiplicity_iff {c d : β} :
emultiplicity a b ≤ emultiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b → c ^ n ∣ d := by
classical
constructor
· exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)
· intro h
unfold emultiplicity
split
next h_1 =>
obtain ⟨w, h_1⟩ := h_1
split
next h_2 =>
simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl, not_true_eq_false,
not_false_eq_true, implies_true]
next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]
next h_1 =>
simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff, dite_eq_right_iff, ENat.coe_ne_top,
imp_false, not_false_eq_true, implies_true]
