OAI/RingTheory/Multiplicity/RootCechProjective.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ProjectiveRoot.gridSectionsEquiv line 15
2. lemma OAI.Lech.ProjectiveRoot.grid_projective line 24
3. lemma OAI.Lech.ProjectiveRoot.zeroAugGrid_projective line 29
4. lemma OAI.Lech.ProjectiveRoot.target_term_projective line 45
5. abbrev OAI.Lech.ProjectiveRoot.integerCech line 56
6. lemma OAI.Lech.ProjectiveRoot.integer_term_projective line 60
7. lemma OAI.Lech.ProjectiveRoot.integer_bounded line 70
8. lemma OAI.Lech.ProjectiveRoot.integer_homology_projective line 78
9. lemma OAI.Lech.ProjectiveRoot.integer_pure line 86
10. def OAI.Lech.ProjectiveRoot.integerCechSplitting line 99