OAI/GroupTheory/PolycyclicRecognition/Algebra/BilinearCentralGroup.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The group defined by a bilinear central cocycle

These coordinate groups provide the two-step case of the nilpotent lattice construction. Integral and real coefficients use exactly the same law.

  1. def OAI.PolycyclicRecognition.BilinearCentralGroup line 17
  2. instance OAI.PolycyclicRecognition.BilinearCentralGroup.(instance at line 22) line 22
  3. theorem OAI.PolycyclicRecognition.BilinearCentralGroup.mul_fst line 46
  4. theorem OAI.PolycyclicRecognition.BilinearCentralGroup.mul_snd line 47
  5. theorem OAI.PolycyclicRecognition.BilinearCentralGroup.one_fst line 49
  6. theorem OAI.PolycyclicRecognition.BilinearCentralGroup.one_snd line 50
  7. def OAI.PolycyclicRecognition.BilinearCentralGroup.projection line 52
  8. theorem OAI.PolycyclicRecognition.BilinearCentralGroup.projection_ker_le_center line 57
  9. instance OAI.PolycyclicRecognition.BilinearCentralGroup.(instance at line 67) line 67
  10. def OAI.PolycyclicRecognition.BilinearCentralGroup.map line 70
  11. theorem OAI.PolycyclicRecognition.BilinearCentralGroup.map_injective line 82