OAI/GroupTheory/PolycyclicRecognition/Lattices/IntegralBilinearLattice.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The Lie lattice attached to an integral bilinear group law

  1. def OAI.PolycyclicRecognition.integralBilinearEmbedding line 12
  2. theorem OAI.PolycyclicRecognition.integralBilinearEmbedding_injective line 24
  3. def OAI.PolycyclicRecognition.integralBilinearLattice line 29
  4. theorem OAI.PolycyclicRecognition.integralBilinearLattice_uniform line 34
  5. def OAI.PolycyclicRecognition.integralBilinearLatticeEquiv line 37
  6. theorem OAI.PolycyclicRecognition.integralBilinear_solvable_realization line 53