multiplicity_le_multiplicity_iff — Mathlib

English

If a finite multiplicity holds for both pairs (a,b) and (c,d), then multiplicity a b ≤ multiplicity c d iff ∀ n, a^n ∣ b → c^n ∣ d.

Русский

Если для пар (a,b) и (c,d) обе пары имеют конечную умножимость, то multiplicity a b ≤ multiplicity c d тогда и только тогда, когда ∀ n, a^n ∣ b → c^n ∣ d.

LaTeX

$$$ \operatorname{multiplicity}(a,b) \le \operatorname{multiplicity}(c,d) \iff \forall n \in \mathbb{N},\ a^n \mid b \Rightarrow c^n \mid d$$$

Lean4

theorem multiplicity_le_multiplicity_iff {c d : β} (hab : FiniteMultiplicity a b) (hcd : FiniteMultiplicity c d) :
    multiplicity a b ≤ multiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b → c ^ n ∣ d :=
  by
  rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hab.emultiplicity_eq_multiplicity, ← hcd.emultiplicity_eq_multiplicity]
  apply emultiplicity_le_emultiplicity_iff

Похожие утверждения