pow_dvd_iff_le_multiplicity — Mathlib

English

If FiniteMultiplicity a b holds, then a^k ∣ b iff k ≤ multiplicity a b.

Русский

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

LaTeX

$$$$FiniteMultiplicity\ a\ b \rightarrow \forall {k: \mathbb{N}}, a^{k} \mid b \leftrightarrow k \le multiplicity a b.$$$$

Lean4

theorem pow_dvd_iff_le_multiplicity (hf : FiniteMultiplicity a b) {k : ℕ} : a ^ k ∣ b ↔ k ≤ multiplicity a b := by
  exact_mod_cast hf.emultiplicity_eq_multiplicity ▸ pow_dvd_iff_le_emultiplicity

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