mem_nonunits_iff

Mathlib.RingTheory.Ideal.Nonunits

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

English

An element a belongs to nonunits α if and only if a is not a unit.

Русский

Элемент a принадлежит к неединицам α тогда и только тогда, когда он не единица.

LaTeX

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

Lean4

@[simp]
theorem mem_nonunits_iff [Monoid α] : a ∈ nonunits α ↔ ¬IsUnit a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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