of_prime_left — Mathlib

English

Let α be a CancelCommutative Monoid with Zero and a be a prime element; if b ≠ 0, then the multiplicity of a in b is finite.

Русский

Пусть α — отменяемый коммутативный моноид с нулём, и a — простая (irreducible) элемента; если b ≠ 0, то кратность a в b конечна.

LaTeX

$$$FiniteMultiplicity(a,b)$$$

Lean4

theorem of_prime_left [CancelCommMonoidWithZero α] [WfDvdMonoid α] {a b : α} (ha : Prime a) (hb : b ≠ 0) :
    FiniteMultiplicity a b :=
  .of_not_isUnit ha.not_unit hb

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