OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalCharacterCancellation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cancelling a rational character on its one-dimensional representation

  1. theorem OAI.PolycyclicRecognition.rationalActionCharacter_action line 14
  2. def OAI.PolycyclicRecognition.rationalScalarMap line 26
  3. theorem OAI.PolycyclicRecognition.rationalScalarMap_apply line 29
  4. theorem OAI.PolycyclicRecognition.rationalTensorAction_cancel line 32