isNilpotent_mul_right

Mathlib.RingTheory.Nilpotent.Defs

URI: https://scilib.ai/kg/mathlib#Commute.isNilpotent_mul_right

← MathLib Explorer

English

If x commutes with y and x is nilpotent, then x y is nilpotent.

Русский

Если x коммутирует с y и x нильпотентен, то x y нильпотентен.

LaTeX

$$Commute x y → IsNilpotent x → IsNilpotent (x y)$$

Lean4

theorem isNilpotent_mul_right (h_comm : Commute x y) (h : IsNilpotent x) : IsNilpotent (x * y) :=
  by
  obtain ⟨n, hn⟩ := h
  use n
  rw [h_comm.mul_pow, hn, zero_mul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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