le_multiplicity_of_pow_dvd — Mathlib

English

If FiniteMultiplicity a b holds and a^k divides b in the HPow sense, then k ≤ multiplicity a b.

Русский

Если FiniteMultiplicity a b и a^k делит b, то k ≤ кратность a b.

LaTeX

$$$$FiniteMultiplicity\ a\ b \rightarrow \forall {k: \mathbb{N}}, semigroupDvd.dvd (instHPow.hPow a k) b \rightarrow k \le multiplicity a b.$$$$

Lean4

theorem le_multiplicity_of_pow_dvd (hf : FiniteMultiplicity a b) {k : ℕ} (hk : a ^ k ∣ b) : k ≤ multiplicity a b :=
  hf.le_multiplicity_of_le_emultiplicity (le_emultiplicity_of_pow_dvd hk)

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