OAI/GroupTheory/PolycyclicRecognition/Algebra/ClassTwoScalarBracket.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Field-valued brackets of the actual central derived layer

  1. def OAI.PolycyclicRecognition.centralDerivedAlternating line 14
  2. theorem OAI.PolycyclicRecognition.centralDerivedAlternating_exterior line 19
  3. def OAI.PolycyclicRecognition.scalarCentralDerivedBracket line 35
  4. theorem OAI.PolycyclicRecognition.scalarCentralDerivedBracket_surjective line 40
  5. theorem OAI.PolycyclicRecognition.scalarCentralDerived_finite line 47
  6. def OAI.PolycyclicRecognition.centralDerivedAddEquiv line 54
  7. theorem OAI.PolycyclicRecognition.classTwo_scalar_derived_finite line 63