neg

Mathlib.RingTheory.Nilpotent.Basic

URI: https://scilib.ai/kg/mathlib#IsNilpotent.neg

English

If x is nilpotent in a ring, then its negation −x is nilpotent as well.

Русский

Если x нильпотент в кольце, то и −x нильпотент.

LaTeX

$$$ \\text{IsNilpotent}(x) \\Rightarrow \\text{IsNilpotent}(-x) $$$

Lean4

theorem neg [Ring R] (h : IsNilpotent x) : IsNilpotent (-x) :=
  by
  obtain ⟨n, hn⟩ := h
  use n
  rw [neg_pow, hn, mul_zero]

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

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

Разделы

Аффилиация

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