OAI/RingTheory/Multiplicity/FrobeniusHomologyGrowth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.free_extendScalars line 14
2. lemma OAI.Lech.finrank_extendScalars line 20
3. instance OAI.Lech.Koszul.moduleQuotient_linear line 28
4. def OAI.Lech.Koszul.quotient_nullhomotopy line 34
5. theorem OAI.Lech.frobenius_quotient_homology_bound line 46