isPrimal

Mathlib.Algebra.GroupWithZero.Submonoid.Primal

URI: https://scilib.ai/kg/mathlib#Submonoid.isPrimal

Lean4

/-- The submonoid of primal elements in a cancellative commutative monoid with zero. -/
def isPrimal (M₀ : Type*) [CancelCommMonoidWithZero M₀] : Submonoid M₀
    where
  carrier := {a | IsPrimal a}
  mul_mem' := .mul
  one_mem' := isUnit_one.isPrimal

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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