OAI/Algebra/FrobeniusObstruction/ResiduePairing.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.MixedForms.oneFormLinear line 13
  2. def OAI.BoundaryOnly.FormalObstruction.MixedForms.exteriorBase line 24
  3. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.exteriorBase_ι line 28
  4. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.alternating_det line 33
  5. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.oneForms_product line 56
  6. def OAI.BoundaryOnly.FormalObstruction.MixedForms.volumeCoeff line 74
  7. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.volumeCoeff_volume line 78
  8. def OAI.BoundaryOnly.FormalObstruction.MixedForms.residue line 94
  9. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.residue_tmul line 97
  10. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.residue_d line 102
  11. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.residue_mul_d line 110
  12. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.mul_delta_of_cycle line 120
  13. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.residue_mul_delta line 130
  14. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.normal_factor line 137
  15. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.normal_append line 147
  16. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.normal_ofFn line 152
  17. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.topMonomial_eq_prod line 180
  18. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.augmentation_partial line 192
  19. abbrev OAI.BoundaryOnly.FormalObstruction.NormalPairing.Scalar line 207
  20. abbrev OAI.BoundaryOnly.FormalObstruction.NormalPairing.OriginalForms line 208
  21. def OAI.BoundaryOnly.FormalObstruction.NormalPairing.res line 210
  22. theorem OAI.BoundaryOnly.FormalObstruction.NormalPairing.jacobian_augmentation line 213
  23. theorem OAI.BoundaryOnly.FormalObstruction.NormalPairing.chart_top_product line 227
  24. theorem OAI.BoundaryOnly.FormalObstruction.NormalPairing.residue_chart_formula line 234
  25. theorem OAI.BoundaryOnly.FormalObstruction.NormalPairing.coordinate_residue_ne_zero line 253
  26. theorem OAI.BoundaryOnly.FormalObstruction.NormalPairing.normals_pair_ne_zero line 265