OAI/Algebra/FrobeniusObstruction/TangentCharts.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentCoeff_eq_augmentation_partial line 14
  2. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.augmentation_natural line 23
  3. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentCoeff_chain_rule line 32
  4. theorem OAI.BoundaryOnly.FormalObstruction.graph_constant_zero line 50
  5. def OAI.BoundaryOnly.FormalObstruction.graphSlot line 60
  6. theorem OAI.BoundaryOnly.FormalObstruction.graphSlot_slope line 71
  7. theorem OAI.BoundaryOnly.FormalObstruction.graphSlot_tangent line 76
  8. def OAI.BoundaryOnly.FormalObstruction.fixedComplement line 81
  9. theorem OAI.BoundaryOnly.FormalObstruction.fixedComplement_augmentation line 86
  10. theorem OAI.BoundaryOnly.FormalObstruction.fixedComplement_pow line 90
  11. def OAI.BoundaryOnly.FormalObstruction.specialChartCoordinate line 96
  12. theorem OAI.BoundaryOnly.FormalObstruction.specialChartCoordinate_pow line 100
  13. def OAI.BoundaryOnly.FormalObstruction.specialChart line 115
  14. theorem OAI.BoundaryOnly.FormalObstruction.specialChart_coordinate line 120
  15. theorem OAI.BoundaryOnly.FormalObstruction.graphSlot_tangentCoeff line 124
  16. theorem OAI.BoundaryOnly.FormalObstruction.fixedComplement_tangentCoeff line 140
  17. theorem OAI.BoundaryOnly.FormalObstruction.specialChart_tangent_matrix line 149
  18. theorem OAI.BoundaryOnly.FormalObstruction.specialChart_bijective line 164
  19. def OAI.BoundaryOnly.FormalObstruction.specialChartEquiv line 170
  20. def OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentJacobian line 181
  21. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentJacobian_comp line 184
  22. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentJacobian_id line 192
  23. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentJacobian_det_unit line 202