OAI/NumberTheory/PiExponent/Cohomology/ProjectiveMonomialCech.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.ProjectiveMonomialCech.Monomial line 16
  2. abbrev OAI.PiExponent.ProjectiveMonomialCech.Laurent line 19
  3. def OAI.PiExponent.ProjectiveMonomialCech.RegularOn line 22
  4. def OAI.PiExponent.ProjectiveMonomialCech.overlapSupport line 25
  5. def OAI.PiExponent.ProjectiveMonomialCech.primitive line 30
  6. theorem OAI.PiExponent.ProjectiveMonomialCech.primitive_apply line 38
  7. theorem OAI.PiExponent.ProjectiveMonomialCech.primitive_support_subset line 42
  8. theorem OAI.PiExponent.ProjectiveMonomialCech.primitive_regular line 48
  9. theorem OAI.PiExponent.ProjectiveMonomialCech.primitive_coboundary line 60
  10. theorem OAI.PiExponent.ProjectiveMonomialCech.exists_primitive_of_pivot line 70
  11. theorem OAI.PiExponent.ProjectiveMonomialCech.exists_nonnegative_coordinate line 80
  12. theorem OAI.PiExponent.ProjectiveMonomialCech.nonnegative_twist_cech_exact line 89