emultiplicity_eq_of_dvd_of_not_dvd

English

If a^k divides b and a^(k+1) does not divide b, then emultiplicity a b = k.

Русский

Если a^k делит b, и не делит b a^(k+1), то эмплитичность a b = k.

LaTeX

$$$$\forall {a,b, k}, a^{k} \mid b \wedge \lnot a^{k+1} \mid b \rightarrow emultiplicity\ a\ b = k.$$$$

Lean4

theorem emultiplicity_eq_of_dvd_of_not_dvd {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) :
    emultiplicity a b = k := by
  classical
  have : FiniteMultiplicity a b := ⟨k, hsucc⟩
  simp only [emultiplicity, this, ↓reduceDIte, Nat.cast_inj, find_eq_iff, hsucc, not_false_eq_true, Decidable.not_not,
    true_and]
  exact fun n hn ↦ (pow_dvd_pow _ hn).trans hk

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