nonunits

Mathlib.RingTheory.Ideal.Nonunits

URI: https://scilib.ai/kg/mathlib#nonunits

English

The set of noninvertible elements of a monoid α is defined by nonunits α = {a ∈ α | ¬IsUnit(a)}.

Русский

Множество неединиц моноида α задаётся как {a ∈ α | ¬IsUnit(a)}.

LaTeX

$$nonunits(\alpha) = \{ a \in \alpha \mid \neg \mathrm{IsUnit}(a) \}$$

Lean4

/-- The set of non-invertible elements of a monoid. -/
def nonunits (α : Type*) [Monoid α] : Set α :=
  {a | ¬IsUnit a}

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

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

Разделы

Аффилиация

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