isNilpotent_toEnd_of_isNilpotent — Mathlib

English

If L acts nilpotently on M, then the endomorphism toEnd x is nilpotent for every x in L.

Русский

Если действие L нильпотентно на M, то toEnd(x) нильпотентно для каждого x ∈ L.

LaTeX

$$∀ x ∈ L, IsNilpotent (toEnd R L M x)$$

Lean4

theorem isNilpotent_toEnd_of_isNilpotent [IsNilpotent L M] (x : L) : _root_.IsNilpotent (toEnd R L M x) :=
  by
  change ∃ k, toEnd R L M x ^ k = 0
  have := exists_forall_pow_toEnd_eq_zero R L M
  tauto

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