OAI/GroupTheory/PolycyclicRecognition/Algebra/CyclicExteriorOrbitDependence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite exterior square excludes a free cyclic orbit over a field

  1. def OAI.PolycyclicRecognition.rationalExteriorSquareRepresentation line 17
  2. theorem OAI.PolycyclicRecognition.rationalExteriorMap_injective line 23
  3. theorem OAI.PolycyclicRecognition.rationalExterior_finite_of_injection line 32
  4. def OAI.PolycyclicRecognition.cyclicOrbitLinearMap line 60
  5. theorem OAI.PolycyclicRecognition.cyclicOrbitLinearMap_equivariant line 64
  6. theorem OAI.PolycyclicRecognition.cyclic_orbit_dependent_of_finite_exterior line 80