OAI/RingTheory/Multiplicity/FrobeniusHomologyFinite.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.finite_shortComplex_homology line 12
2. lemma OAI.Lech.finite_cochain_homology line 20
3. lemma OAI.Lech.shortComplex_nullScalar_radical line 28
4. lemma OAI.Lech.shortComplex_uniform_nullhomotopy line 40
5. lemma OAI.Lech.finiteLength_of_maximal_le_radical_annihilator line 48
6. theorem OAI.Lech.frobenius_shortComplex_homology_finiteLength line 58