pow_dvd_iff_le_emultiplicity — Mathlib

English

For any k, a^k divides b if and only if k ≤ emultiplicity a b.

Русский

Для любого k, a^k делит b тогда и только тогда, когда k ≤ эмплитичность a b.

LaTeX

$$$$\forall {\alpha} [Monoid \alpha], {a,b: \alpha}, {k: \mathbb{N}}, a^{k} \mid b \leftrightarrow k \le emultiplicity a b.$$$$

Lean4

theorem pow_dvd_iff_le_emultiplicity {k : ℕ} : a ^ k ∣ b ↔ k ≤ emultiplicity a b :=
  ⟨le_emultiplicity_of_pow_dvd, pow_dvd_of_le_emultiplicity⟩

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