irreducible_iff_prime — Mathlib

English

In a Decomposition Monoid M, an element a is irreducible if and only if it is prime.

Русский

В декомпозиционном моноиде M элемент a является ирредуцируемым тогда и только тогда, когда он простой.

LaTeX

$$$\\forall a : M,\\; \\operatorname{Irreducible}(a) \\iff \\operatorname{Prime}(a).$$$

Lean4

theorem irreducible_iff_prime [DecompositionMonoid M] {a : M} : Irreducible a ↔ Prime a :=
  ⟨Irreducible.prime, Prime.irreducible⟩

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