OAI/RingTheory/Multiplicity/FiniteModuleCech.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Lech.FiniteModuleCech.Diagram line 15
2. abbrev OAI.Lech.FiniteModuleCech.cochains line 24
3. def OAI.Lech.FiniteModuleCech.d line 26
4. lemma OAI.Lech.FiniteModuleCech.raw_square line 41
5. def OAI.Lech.FiniteModuleCech.toFixed line 53
6. lemma OAI.Lech.FiniteModuleCech.toFixed_d line 57
7. lemma OAI.Lech.FiniteModuleCech.d_square line 72
8. def OAI.Lech.FiniteModuleCech.complex line 87
9. lemma OAI.Lech.FiniteModuleCech.complex_d line 94
10. lemma OAI.Lech.FiniteModuleCech.bounded line 99
11. structure OAI.Lech.FiniteModuleCech.Map line 108
12. def OAI.Lech.FiniteModuleCech.Map.cochains line 114
13. lemma OAI.Lech.FiniteModuleCech.Map.cochains_d line 119
14. def OAI.Lech.FiniteModuleCech.Map.complex line 135