emultiplicity_le_of_multiplicity_le

English

If FiniteMultiplicity a b, then for any n, multiplicity a b ≤ n implies emultiplicity a b ≤ n.

Русский

Если FiniteMultiplicity a b, то для любого n, если multiplicity a b ≤ n, то emultiplicity a b ≤ n.

LaTeX

$$$ h_{fin} : FiniteMultiplicity(a,b) \to (\forall n, multiplicity(a,b) \le n \to emultiplicity(a,b) \le n) $$$

Lean4

theorem emultiplicity_le_of_multiplicity_le (hfin : FiniteMultiplicity a b) {n : ℕ} (h : multiplicity a b ≤ n) :
    emultiplicity a b ≤ n := by
  rw [emultiplicity_eq_multiplicity hfin]
  assumption_mod_cast

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