OAI/NumberTheory/PiExponent/Cohomology/GradedCechBound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.FiniteTupleCech.Cochain line 17
  2. def OAI.PiExponent.FiniteTupleCech.differential line 19
  3. lemma OAI.PiExponent.FiniteTupleCech.differential_zero line 23
  4. lemma OAI.PiExponent.FiniteTupleCech.differential_add line 27
  5. lemma OAI.PiExponent.FiniteTupleCech.differential_sub line 32
  6. lemma OAI.PiExponent.FiniteTupleCech.mem_tupleSet line 37
  7. def OAI.PiExponent.FiniteTupleCech.liftTo line 40
  8. def OAI.PiExponent.FiniteTupleCech.evaluate line 43
  9. lemma OAI.PiExponent.FiniteTupleCech.evaluate_differential line 48
  10. lemma OAI.PiExponent.FiniteTupleCech.differential_squared line 57
  11. lemma OAI.PiExponent.FiniteTupleCech.tuple_card_lt_of_missing line 66
  12. def OAI.PiExponent.FiniteTupleCech.assemble line 76
  13. lemma OAI.PiExponent.FiniteTupleCech.assemble_restrict line 82
  14. lemma OAI.PiExponent.FiniteTupleCech.differential_assemble_below line 103
  15. theorem OAI.PiExponent.FiniteTupleCech.level_correction line 117
  16. theorem OAI.PiExponent.FiniteTupleCech.primitives line 159
  17. theorem OAI.PiExponent.GradedCechBound.primitives line 205