le_emultiplicity_of_pow_dvd — Mathlib

English

If a^k divides b (in a semigroup sense), then k ≤ emultiplicity a b.

Русский

Если a^k делит b (в смысле полугруппы), то k ≤ эмплитичность a b.

LaTeX

$$$$\forall {\alpha} [Monoid \alpha], {a,b: \alpha}, {k: \mathbb{N}}, semigroupDvd.dvd (instHPow.hPow a k) b \rightarrow k \le emultiplicity a b.$$$$

Lean4

theorem le_emultiplicity_of_pow_dvd {k : ℕ} (hk : a ^ k ∣ b) : k ≤ emultiplicity a b :=
  le_of_not_gt fun hk' => not_pow_dvd_of_emultiplicity_lt hk' hk

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