OAI/Algebra/FrobeniusObstruction/ChartPairing.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.equiv_cartier line 15
  2. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.equiv_normal line 20
  3. def OAI.BoundaryOnly.FormalObstruction.swapEquiv line 33
  4. theorem OAI.BoundaryOnly.FormalObstruction.swapEquiv_apply line 39
  5. theorem OAI.BoundaryOnly.FormalObstruction.swapEquiv_symm line 42
  6. theorem OAI.BoundaryOnly.FormalObstruction.complementaryMatrix_swap line 44
  7. theorem OAI.BoundaryOnly.FormalObstruction.inverseChart_tangent line 51
  8. theorem OAI.BoundaryOnly.FormalObstruction.inverseChart_tangent_swap line 66
  9. theorem OAI.BoundaryOnly.FormalObstruction.tangentCoeff_swap line 78
  10. def OAI.BoundaryOnly.FormalObstruction.jointNormalCoordinate line 95
  11. theorem OAI.BoundaryOnly.FormalObstruction.jointNormalCoordinate_pow line 101
  12. def OAI.BoundaryOnly.FormalObstruction.jointNormalChart line 106
  13. theorem OAI.BoundaryOnly.FormalObstruction.jointNormalChart_coordinate line 111
  14. theorem OAI.BoundaryOnly.FormalObstruction.jointNormalChart_tangent line 115
  15. theorem OAI.BoundaryOnly.FormalObstruction.jointNormalChart_bijective line 126
  16. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.reindex_mk line 139
  17. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.embDomain_top line 154
  18. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.topCoeff_reindex line 161
  19. def OAI.BoundaryOnly.FormalObstruction.MixedForms.fixedResidue line 175
  20. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.fixedResidue_tmul line 180
  21. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.fixedResidue_d line 184
  22. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.fixedResidue_mul_d line 191
  23. theorem OAI.BoundaryOnly.FormalObstruction.FormsReindex.residue_equiv line 206
  24. def OAI.BoundaryOnly.FormalObstruction.fullNormalIndexList line 222
  25. theorem OAI.BoundaryOnly.FormalObstruction.fullNormalIndexList_nodup line 225
  26. theorem OAI.BoundaryOnly.FormalObstruction.mem_fullNormalIndexList line 237
  27. def OAI.BoundaryOnly.FormalObstruction.normalEnumeration line 247
  28. theorem OAI.BoundaryOnly.FormalObstruction.normalEnumeration_list line 252
  29. def OAI.BoundaryOnly.FormalObstruction.negativeNormal line 264
  30. theorem OAI.BoundaryOnly.FormalObstruction.jointNormal_list line 268
  31. theorem OAI.BoundaryOnly.FormalObstruction.specialNormal_product line 287
  32. def OAI.BoundaryOnly.FormalObstruction.finiteNormalChart line 295
  33. theorem OAI.BoundaryOnly.FormalObstruction.finiteNormalChart_coordinate line 302
  34. theorem OAI.BoundaryOnly.FormalObstruction.specialNormal_product_reindex line 311
  35. theorem OAI.BoundaryOnly.FormalObstruction.specialNormal_pairing line 333