one_notMem_nonunits

Mathlib.RingTheory.Ideal.Nonunits

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

English

One is not a nonunit; i.e., 1 ∉ nonunits α.

Русский

Единица не является неединицей; то есть 1 ∉ nonunits α.

LaTeX

$$1 \notin nonunits(\alpha)$$

Lean4

@[simp high] -- High priority shortcut lemma

theorem one_notMem_nonunits [Monoid α] : (1 : α) ∉ nonunits α :=
  not_not_intro isUnit_one

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

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

Разделы

Аффилиация

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