zero_lt_finrank_genWeightSpace — Mathlib

English

If there exists a simultaneous generalized eigenvector for the L-action, then there is a nonzero eigenvector m with [x,m] = χ(x)m for all x in L, provided M is Noetherian and has linear weights.

Русский

Если существует общий обобщённый собственный вектор для действия L, то существует ненулевой собственный вектор m с [x,m] = χ(x)m для всех x в L, если M конечно порождается и имеет линейные веса.

LaTeX

$$$\\exists m\\neq 0,\\; \\forall x\\in L,\\; [x,m]=χ(x)\\,m.$$$

Lean4

theorem zero_lt_finrank_genWeightSpace {χ : L → R} (hχ : genWeightSpace M χ ≠ ⊥) : 0 < finrank R (genWeightSpace M χ) :=
  by
  rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank, Nat.cast_pos] at hχ

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