emultiplicity_eq_ofNat — Mathlib

English

If n ∈ ℕ with n ≥ 2, then emultiplicity a b = ofNat(n) in ℕ∞ holds exactly when a^n ∣ b and a^(n+1) ∤ b.

Русский

Пусть n ∈ ℕ и n ≥ 2. Тогда emultiplicity a b = ofNat(n) в ℕ∞ эквивалентно тому, что a^n делит b, и a^(n+1) не делит b.

LaTeX

$$$ (n \ge 2) \Rightarrow \operatorname{emultiplicity}(a,b) = \mathrm{ofNat}(n) \iff a^n \mid b \land \neg a^{n+1} \mid b $$$

Lean4

theorem emultiplicity_eq_ofNat {a b n : ℕ} [n.AtLeastTwo] :
    emultiplicity a b = (ofNat(n) : ℕ∞) ↔ a ^ ofNat(n) ∣ b ∧ ¬a ^ (ofNat(n) + 1) ∣ b :=
  emultiplicity_eq_coe

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