isNilpotent_C_mul_pow_X_of_isNilpotent

English

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

Русский

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

LaTeX

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

Lean4

theorem isNilpotent_C_mul_pow_X_of_isNilpotent (n : ℕ) (hnil : IsNilpotent r) : IsNilpotent ((C r) * X ^ n) :=
  by
  refine Commute.isNilpotent_mul_right (commute_X_pow _ _).symm ?_
  obtain ⟨m, hm⟩ := hnil
  refine ⟨m, ?_⟩
  rw [← C_pow, hm, C_0]

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