OAI/GroupTheory/PolycyclicRecognition/Algebra/BoundedWordAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite algebras from a bound on generator products

This is the finite-dimensionality step for the truncated enveloping algebra used to extend a nilpotent representation by derivations.

  1. def OAI.PolycyclicRecognition.boundedWordProducts line 23

    Source documentation

    Products with at most the specified number of letters.

    def boundedWordProducts : Set A :=
…
  2. theorem OAI.PolycyclicRecognition.boundedWordProducts_finite line 26
  3. theorem OAI.PolycyclicRecognition.list_prod_mem_boundedWordSpan line 30
  4. theorem OAI.PolycyclicRecognition.adjoin_le_boundedWordSpan line 42
  5. theorem OAI.PolycyclicRecognition.finiteDimensional_of_bounded_generator_products line 62