OAI/GroupTheory/PolycyclicRecognition/Geometry/WeightBasisTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Trace in an arbitrary generalized-weight basis

Bracket-word bases need not triangularize the nilpotent parts of the Cartan action. The trace is nevertheless the sum of their weights. We prove this by separating the scalar action on each generalized weight space; the residual operator has zero trace on every such space.

  1. theorem OAI.PolycyclicRecognition.trace_eq_sum_of_generalizedWeight_basis line 26