OAI/Algebra/FrobeniusObstruction/TopResidue.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.Frobenius.reindex line 14
  2. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.reindex_coordinate line 19
  3. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_reindex line 23
  4. def OAI.BoundaryOnly.FormalObstruction.FormsReindex.vec line 56
  5. def OAI.BoundaryOnly.FormalObstruction.FormsReindex.exterior line 59
  6. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.exterior_gen line 65
  7. abbrev OAI.BoundaryOnly.FormalObstruction.FormsReindex.QForms line 79
  8. def OAI.BoundaryOnly.FormalObstruction.FormsReindex.equiv line 82
  9. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.equiv_tmul line 85
  10. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.equiv_d line 89
  11. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.equiv_coeff line 100
  12. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.equiv_gradient line 106
  13. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.equiv_delta line 112
  14. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.quotientCoeff_coordinate_mul line 126
  15. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.eq_smul_top_of_coordinate_annihilate line 139
  16. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.automorphism_top line 175