prime

Mathlib.Algebra.Prime.Defs

URI: https://scilib.ai/kg/mathlib#Irreducible.prime

English

If M is a DecompositionMonoid, then an irreducible element is prime.

Русский

Если M является декомпозиционным моноидом, то несводимый элемент является простым.

LaTeX

$$∀ a, Irreducible a → Prime a$$

Lean4

theorem prime [DecompositionMonoid M] {a : M} (irr : Irreducible a) : Prime a :=
  irr.prime_of_isPrimal (DecompositionMonoid.primal a)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru