not_pow_dvd_of_emultiplicity_lt — Mathlib

English

If emultiplicity a b < m, then a^m does not divide b.

Русский

Если emultiplicity a b < m, то a^m не делит b.

LaTeX

$$$$\forall {\alpha} [Monoid \alpha], {a,b: \alpha}, {m: \mathbb{N}}, emultiplicity a b < m \rightarrow \lnot (a^{m} \mid b).$$$$

Lean4

theorem not_pow_dvd_of_emultiplicity_lt {m : ℕ} (hm : emultiplicity a b < m) : ¬a ^ m ∣ b := fun nh =>
  by
  unfold emultiplicity at hm
  split at hm
  · simp only [cast_lt, find_lt_iff] at hm
    obtain ⟨n, hn1, hn2⟩ := hm
    exact hn2 ((pow_dvd_pow _ hn1).trans nh)
  · simp at hm

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