OAI/GroupTheory/PolycyclicRecognition/Algebra/ScalarH2BilinearDetection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bilinear coordinates detect the scalar-extended exterior cross product

  1. def OAI.PolycyclicRecognition.scalarH2DetectorPairing line 14
  2. def OAI.PolycyclicRecognition.scalarH2Detector line 24
  3. theorem OAI.PolycyclicRecognition.scalarH2Detector_class line 29
  4. theorem OAI.PolycyclicRecognition.scalarH2Detector_pairing line 43
  5. theorem OAI.PolycyclicRecognition.scalarH2Detector_exterior line 67
  6. theorem OAI.PolycyclicRecognition.scalarExtendedH2ExteriorProduct_injective line 84