zero_mem_nonunits

Mathlib.RingTheory.Ideal.Nonunits

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

English

In a monoid with zero, 0 is a nonunit if and only if 0 ≠ 1.

Русский

В моноиде с нулём 0 является неединицей тогда и только тогда, когда 0 ≠ 1.

LaTeX

$$0 \in nonunits(\alpha) \iff 0 \neq 1$$

Lean4

theorem zero_mem_nonunits [MonoidWithZero α] : 0 ∈ nonunits α ↔ (0 : α) ≠ 1 :=
  not_congr isUnit_zero_iff

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

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

Разделы

Аффилиация

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