not_pow_dvd_of_multiplicity_lt — Mathlib

English

If FiniteMultiplicity a b and multiplicity a b < m, then a^m does not divide b.

Русский

Если FiniteMultiplicity a b и кратность a b < m, то a^m не делит b.

LaTeX

$$$$FiniteMultiplicity\ a\ b \rightarrow \forall {m: \mathbb{N}},\; multiplicity\ a\ b < m \rightarrow \lnot (a^{m} \mid b).$$$$

Lean4

theorem not_pow_dvd_of_multiplicity_lt (hf : FiniteMultiplicity a b) {m : ℕ} (hm : multiplicity a b < m) : ¬a ^ m ∣ b :=
  by
  apply not_pow_dvd_of_emultiplicity_lt
  rw [hf.emultiplicity_eq_multiplicity]
  norm_cast

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