isNilpotent_pow_X_mul_C_of_isNilpotent

Mathlib.RingTheory.Polynomial.Nilpotent

URI: https://scilib.ai/kg/mathlib#Polynomial.isNilpotent_pow_X_mul_C_of_isNilpotent

← MathLib Explorer

English

If r is nilpotent, then X^n · C(r) is nilpotent for any n.

Русский

Если r нильпотентно, то X^n · C(r) нильпотентно для любого n.

LaTeX

$$IsNilpotent(X^n · C(r)) if IsNilpotent r$$

Lean4

theorem isNilpotent_pow_X_mul_C_of_isNilpotent (n : ℕ) (hnil : IsNilpotent r) : IsNilpotent (X ^ n * (C r)) :=
  by
  rw [commute_X_pow]
  exact isNilpotent_C_mul_pow_X_of_isNilpotent n hnil

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

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

Разделы

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

Аффилиация

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