OAI/Algebra/FrobeniusObstruction/ActualBlocks.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.ActualBlocks.Variables line 15
  2. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.grouping line 17
  3. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.coordinates line 23
  4. abbrev OAI.BoundaryOnly.FormalObstruction.ActualBlocks.Scalar line 28
  5. abbrev OAI.BoundaryOnly.FormalObstruction.ActualBlocks.Block line 29
  6. abbrev OAI.BoundaryOnly.FormalObstruction.ActualBlocks.Ambient line 30
  7. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.includeScalar line 32
  8. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.includeBlock line 36
  9. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.reindex_insertScalar line 42
  10. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.includeBlock_coeff line 58
  11. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.wall line 63
  12. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.include_wall line 72
  13. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.blockPotential line 85
  14. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.blockSlope line 89
  15. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.include_blockSlope line 93
  16. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.reindex_potential line 102
  17. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.tensorToForms line 114
  18. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.tensorToForms_tprod line 120
  19. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.tensorToForms_D line 129
  20. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.tensorToForms_delta line 138
  21. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.d_includeBlock line 149
  22. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.gradient_includeScalar line 155
  23. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.delta_includeBlock line 161
  24. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.list_prod_coeff_mul line 174
  25. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.left_cycle_mul_delta line 185
  26. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.tensorToForms_S line 204