pow_succ

Mathlib.RingTheory.Nilpotent.Defs

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

← MathLib Explorer

English

If x is nilpotent, then x^(n+1) is nilpotent for any n.

Русский

Если x нилпотентен, то x^(n+1) нилпотентен для любого n.

LaTeX

$$$ (\\IsNilpotent(x)) \\Rightarrow (\\IsNilpotent(x^{n+1})) $$$

Lean4

theorem pow_succ (n : ℕ) {S : Type*} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) : IsNilpotent (x ^ n.succ) :=
  by
  obtain ⟨N, hN⟩ := hx
  use N
  rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]

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

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

Разделы

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

Аффилиация

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