pow_dvd_of_le_emultiplicity — Mathlib

English

If k ≤ emultiplicity a b, then a^k divides b.

Русский

Если k ≤ emultiplicity a b, то a^k делит b.

LaTeX

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

Lean4

theorem pow_dvd_of_le_emultiplicity {k : ℕ} (hk : k ≤ emultiplicity a b) : a ^ k ∣ b := by
  classical
  cases k
  · simp
  unfold emultiplicity at hk
  split at hk
  · norm_cast at hk
    simpa using (Nat.find_min _ (lt_of_succ_le hk))
  · apply FiniteMultiplicity.not_iff_forall.mp ‹_›

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