OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentSpanningOperators.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent operators spanning a complex nilpotent Lie algebra

Every weight vanishes on the spanning set, hence on the entire Lie algebra. The zero weight space is therefore the whole representation.

  1. theorem OAI.PolycyclicRecognition.nilpotent_operators_of_spanning_set line 19