dvd_iff_multiplicity_pos — Mathlib

English

For any a,b in a monoid, the multiplicity of a in b is positive if and only if a divides b.

Русский

Для любых a,b в моноиде кратность a в b положительна тогда и только тогда, когда a делит b.

LaTeX

$$$0 < \operatorname{multiplicity}(a,b) \iff a \mid b$$$

Lean4

theorem dvd_iff_multiplicity_pos {a b : α} : 0 < multiplicity a b ↔ a ∣ b :=
  ⟨dvd_of_multiplicity_pos, fun hdvd => Nat.pos_of_ne_zero (by simpa [multiplicity_eq_zero])⟩

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