isNilpotent_neg_iff

Mathlib.RingTheory.Nilpotent.Basic

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

English

In a ring, x is nilpotent iff −x is nilpotent.

Русский

В кольце x нильпотентно тогда и только тогда, когда −x нильпотентно.

LaTeX

$$$ \\text{IsNilpotent}(-x) \\;\\leftrightarrow\\; \\text{IsNilpotent}(x) $$$

Lean4

@[simp]
theorem isNilpotent_neg_iff [Ring R] : IsNilpotent (-x) ↔ IsNilpotent x :=
  ⟨fun h => neg_neg x ▸ h.neg, fun h => h.neg⟩

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

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

Разделы

Аффилиация

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