emultiplicity_eq_zero — Mathlib

English

emultiplicity a b = 0 if and only if a does not divide b.

Русский

emultiplicity a b = 0 эквивалентно тому, что a не делит b.

LaTeX

$$$ \operatorname{emultiplicity}(a,b) = 0 \iff \lnot a \mid b $$$

Lean4

theorem emultiplicity_eq_zero : emultiplicity a b = 0 ↔ ¬a ∣ b :=
  by
  by_cases hf : FiniteMultiplicity a b
  · rw [← ENat.coe_zero, emultiplicity_eq_coe]
    simp
  · simpa [emultiplicity_eq_top.2 hf] using FiniteMultiplicity.not_iff_forall.1 hf 1

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