not_isNilpotent_one

Mathlib.RingTheory.Nilpotent.Defs

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

English

In a nontrivial monoid with zero, 1 is not nilpotent.

Русский

В ненулевом моноиде с нулём единица не нилпотентна.

LaTeX

$$$\\neg \\IsNilpotent(1)$$$

Lean4

theorem not_isNilpotent_one [MonoidWithZero R] [Nontrivial R] : ¬IsNilpotent (1 : R) := fun ⟨_, H⟩ ↦
  zero_ne_one (H.symm.trans (one_pow _))

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

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

Разделы

Аффилиация

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