OAI/RingTheory/Multiplicity/CyclicDutta.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.tensor_quotient_homology_length line 31
2. def OAI.Lech.cyclicDuttaSequence line 39
3. lemma OAI.Lech.cyclicDuttaSequence_full line 44
4. lemma OAI.Lech.cyclicDuttaSequence_small line 57
5. def OAI.Lech.cyclicDuttaContribution line 81
6. lemma OAI.Lech.cyclicDuttaSequence_tendsto line 93
7. lemma OAI.Lech.cyclicDuttaContribution_lower line 111