OAI/GroupTheory/PolycyclicRecognition/Algebra/ScalarAlternatingExtension.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Alternation survives scalar extension, including in characteristic two

  1. theorem OAI.PolycyclicRecognition.scalarMultilinearExtension_swap line 14
  2. theorem OAI.PolycyclicRecognition.scalarMultilinearExtension_unit_diagonal line 30
  3. theorem OAI.PolycyclicRecognition.scalarMultilinearExtension_diagonal line 52
  4. def OAI.PolycyclicRecognition.scalarAlternatingExtension line 76
  5. theorem OAI.PolycyclicRecognition.scalarAlternatingExtension_unit line 86