OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentFaithfulRepresentation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A faithful nilpotent matrix representation of a real nilpotent algebra

The coordinate model and its regular representation have both been constructed without a published-input hypothesis. Engel gives a uniform product bound.

  1. theorem OAI.PolycyclicRecognition.exists_faithful_nilpotent_representation line 17