OAI/GroupTheory/PolycyclicRecognition/Analysis/IntegralBilinearRealization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Realizing any bilinear integral central extension

  1. theorem OAI.PolycyclicRecognition.coefficientBilinear_eq line 12
  2. theorem OAI.PolycyclicRecognition.bilinearIntegral_solvable_realization line 23