multiplicity_lt_iff_not_dvd — Mathlib

English

Let hf be a finite multiplicity relation for a and b. Then for every natural k, multiplicity a b < k is equivalent to a^k ∤ b.

Русский

Пусть существует конечная умножимость a в b. Тогда для каждого натурального k верно: multiplicity a b < k эквивалентно тому, что a^k не делит b.

LaTeX

$$$ \operatorname{multiplicity}(a,b) < k \iff \neg a^k \mid b $$$

Lean4

theorem multiplicity_lt_iff_not_dvd {k : ℕ} (hf : FiniteMultiplicity a b) : multiplicity a b < k ↔ ¬a ^ k ∣ b := by
  rw [hf.pow_dvd_iff_le_multiplicity, not_le]

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