dvd_of_multiplicity_pos — Mathlib

English

Let a and b be elements of a monoid. If the multiplicity of a in b is positive, then a divides b.

Русский

Пусть a и b — элементы моноида. Если кратность a в b положительна, то a делит b.

LaTeX

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

Lean4

theorem dvd_of_multiplicity_pos {a b : α} (h : 0 < multiplicity a b) : a ∣ b :=
  dvd_of_emultiplicity_pos (lt_emultiplicity_of_lt_multiplicity h)

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