exists_forall_pow_toEnd_eq_zero — Mathlib

English

There exists a natural number k such that for every x in L, the k-th power of toEnd(x) is zero as an endomorphism of M.

Русский

Существует натуральное число k такое, что для каждого x в L, к-я степень toEnd(x) тождественно ноль на M.

LaTeX

$$∃ k, ∀ x ∈ L, toEnd(R,L,M)(x)^{k} = 0$$

Lean4

theorem exists_forall_pow_toEnd_eq_zero [IsNilpotent L M] : ∃ k : ℕ, ∀ x : L, toEnd R L M x ^ k = 0 :=
  by
  obtain ⟨k, hM⟩ := IsNilpotent.nilpotent R L M
  use k
  intro x; ext m
  rw [Module.End.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]
  exact iterate_toEnd_mem_lowerCentralSeries R L M x m k

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