associates_irreducible_iff_prime — Mathlib

English

For p ∈ Associates M with M a decomposition monoid, irreducible p iff prime p.

Русский

Для p ∈ Associates(M) при M, являющемся разложимым моноидом, неразложимость p эквивалентна простоте p.

LaTeX

$$$ \operatorname{Irreducible}(p) \iff \operatorname{Prime}(p) $$$

Lean4

theorem _root_.associates_irreducible_iff_prime [DecompositionMonoid M] {p : Associates M} : Irreducible p ↔ Prime p :=
  irreducible_iff_prime

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