OAI/GroupTheory/PolycyclicRecognition/Algebra/ScalarExteriorSurjection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar extension preserves a surjective exterior presentation

This uses the integral generators of the exterior power, so it requires no factorial inversion or freeness assumption.

  1. def OAI.PolycyclicRecognition.scalarExteriorPresentation line 18
  2. theorem OAI.PolycyclicRecognition.scalarExteriorPresentation_unit line 23
  3. theorem OAI.PolycyclicRecognition.scalarExteriorPresentation_range_unit line 32
  4. theorem OAI.PolycyclicRecognition.scalarExteriorPresentation_surjective line 53