multiplicity_eq_of_dvd_of_not_dvd

English

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

Русский

Если a^k делит b, и не делит b a^(k+1), то кратность a b = k.

LaTeX

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

Lean4

theorem multiplicity_eq_of_dvd_of_not_dvd {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) : multiplicity a b = k :=
  multiplicity_eq_of_emultiplicity_eq_some (emultiplicity_eq_of_dvd_of_not_dvd hk hsucc)

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