OAI/RingTheory/Multiplicity/RootSectionDiagram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Lech.ProjectiveRoot.CechSection line 13
2. abbrev OAI.Lech.ProjectiveRoot.cechObj line 15
3. def OAI.Lech.ProjectiveRoot.cechRes line 18
4. lemma OAI.Lech.ProjectiveRoot.cechRes_apply line 28
5. lemma OAI.Lech.ProjectiveRoot.cechRes_self line 34
6. lemma OAI.Lech.ProjectiveRoot.cechRes_comp line 42
7. def OAI.Lech.ProjectiveRoot.cechDiagram line 62
8. abbrev OAI.Lech.ProjectiveRoot.zeroAugGrid line 68
9. def OAI.Lech.ProjectiveRoot.gridCechEquiv line 71
10. lemma OAI.Lech.ProjectiveRoot.gridCechEquiv_natural line 97
11. def OAI.Lech.ProjectiveRoot.gridComplexIso line 120