maxGenEigenSpace_toEnd_eq_top — Mathlib

English

For a nilpotent Lie module, the maximal generalized eigen-space for eigenvalue 0 of each endomorphism toEnd x is the entire module M.

Русский

Для нильпотентного модуля максимальное обобщенное собственное подпространство для собственного значения 0 тождественно равно M.

LaTeX

$$toEnd(R,L,M,x).maxGenEigenspace 0 = ⊤$$

Lean4

@[simp]
theorem maxGenEigenSpace_toEnd_eq_top [IsNilpotent L M] (x : L) : ((toEnd R L M x).maxGenEigenspace 0) = ⊤ :=
  by
  ext m
  simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, Submodule.mem_top, iff_true]
  obtain ⟨k, hk⟩ := exists_forall_pow_toEnd_eq_zero R L M
  exact ⟨k, by simp [hk x]⟩

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