isNilpotent_mul_left

Mathlib.RingTheory.Nilpotent.Defs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem isNilpotent_mul_left (h_comm : Commute x y) (h : IsNilpotent y) : IsNilpotent (x * y) :=
  by
  rw [h_comm.eq]
  exact h_comm.symm.isNilpotent_mul_right h

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

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

Разделы

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

Аффилиация

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