OAI/Algebra/FrobeniusObstruction/Coordinates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.Frobenius.includeVariables line 15
  2. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.includeVariables_coordinate line 20
  3. def OAI.BoundaryOnly.FormalObstruction.Frobenius.merge line 24
  4. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.merge_tmul line 31
  5. def OAI.BoundaryOnly.FormalObstruction.Frobenius.splitCoordinates line 36
  6. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.splitCoordinates_pow line 42
  7. def OAI.BoundaryOnly.FormalObstruction.Frobenius.splitBlocks line 50
  8. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.split_coordinate line 55
  9. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.split_includeVariables_left line 60
  10. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.split_includeVariables_right line 69
  11. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.merge_split line 77
  12. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.split_merge line 85
  13. def OAI.BoundaryOnly.FormalObstruction.Frobenius.sumEquiv line 100