OAI/GroupTheory/PolycyclicRecognition/Geometry/UnitsLieAlgebra.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual tangent Lie algebra of algebra units

Differentiating the inclusion identifies the tangent Lie algebra with the commutator algebra. This permits the proved nilpotent integration theorem to target matrix units directly.

  1. def OAI.PolycyclicRecognition.unitsLieHom line 22
  2. theorem OAI.PolycyclicRecognition.unitsLieHom_apply line 25
  3. def OAI.PolycyclicRecognition.unitsLieEquiv line 31
  4. theorem OAI.PolycyclicRecognition.unitsLieEquiv_apply line 36
  5. theorem OAI.PolycyclicRecognition.unitsLieEquiv_symm_apply line 39
  6. theorem OAI.PolycyclicRecognition.groupExponential_units line 45