OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalFiniteQuotient.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rational dimension under a finite normal quotient

  1. def OAI.PolycyclicRecognition.RationalQuotient.normalCoinvariantsInflationCounit line 15
  2. theorem OAI.PolycyclicRecognition.RationalQuotient.normalCoinvariantsInflationCounit_mk line 33
  3. def OAI.PolycyclicRecognition.RationalQuotient.normalCoinvariantsInflationAdjunction line 37
  4. instance OAI.PolycyclicRecognition.RationalQuotient.normalCoinvariants_preservesProjective line 62
  5. instance OAI.PolycyclicRecognition.RationalQuotient.quotientCoinvariants_additive line 68
  6. instance OAI.PolycyclicRecognition.RationalQuotient.(instance at line 76) line 76
  7. instance OAI.PolycyclicRecognition.RationalQuotient.(instance at line 79) line 79
  8. instance OAI.PolycyclicRecognition.RationalQuotient.(instance at line 88) line 88
  9. theorem OAI.PolycyclicRecognition.RationalQuotient.exactFunctor_rational_dimension line 99
  10. def OAI.PolycyclicRecognition.RationalQuotient.trivialCoinvariantsIso line 125
  11. theorem OAI.PolycyclicRecognition.RationalQuotient.rational_dimension_quotient line 144
  12. theorem OAI.PolycyclicRecognition.RationalQuotient.rational_dimension_subgroup line 153