OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianNormalExteriorInjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

FP-infinity controls all exterior degrees in every characteristic

  1. def OAI.PolycyclicRecognition.scalarAbelianNormalExteriorInjection line 16
  2. theorem OAI.PolycyclicRecognition.typeFPInfinity_abelianNormalHigherExterior_finite_all_char line 24