OAI/NumberTheory/PiExponent/Geometry/ProjectiveMonomialFinite.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ProjectiveMonomialFinite.AllNegative line 14
2. theorem OAI.PiExponent.ProjectiveMonomialFinite.allNegative_coordinate_bounds line 16
3. instance OAI.PiExponent.ProjectiveMonomialFinite.allNegative_finite line 27
4. instance OAI.PiExponent.ProjectiveMonomialFinite.allNonnegative_finite line 37
5. instance OAI.PiExponent.ProjectiveMonomialFinite.monomial_subsingleton line 55
6. def OAI.PiExponent.ProjectiveMonomialFinite.filterCochain line 70
7. theorem OAI.PiExponent.ProjectiveMonomialFinite.filterCochain_apply line 75
8. theorem OAI.PiExponent.ProjectiveMonomialFinite.filterCochain_regular line 81
9. theorem OAI.PiExponent.ProjectiveMonomialFinite.differential_filterCochain line 91
10. theorem OAI.PiExponent.ProjectiveMonomialFinite.filterCochain_closed line 102
11. theorem OAI.PiExponent.ProjectiveMonomialFinite.exact_of_obstruction_zero line 110
12. theorem OAI.PiExponent.ProjectiveMonomialFinite.cocycle_eq_boundary_add_negative line 151