OAI/Geometry/TamingCompatibility/Hodge/HodgeStarGeometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HodgeStarGeometry.starMap line 19
  2. lemma OAI.TamingCompatibility.HodgeStarGeometry.starMap_apply line 23
  3. lemma OAI.TamingCompatibility.HodgeStarGeometry.starMap_adjoint line 24
  4. def OAI.TamingCompatibility.HodgeStarGeometry.swap line 28
  5. def OAI.TamingCompatibility.HodgeStarGeometry.swapMap line 29
  6. lemma OAI.TamingCompatibility.HodgeStarGeometry.swapMap_apply line 33
  7. lemma OAI.TamingCompatibility.HodgeStarGeometry.swapMap_adjoint line 34
  8. lemma OAI.TamingCompatibility.HodgeStarGeometry.principal_intertwines line 41
  9. lemma OAI.TamingCompatibility.HodgeStarGeometry.swap_join line 48
  10. lemma OAI.TamingCompatibility.HodgeStarGeometry.swap_left line 51
  11. lemma OAI.TamingCompatibility.HodgeStarGeometry.swap_right line 54
  12. lemma OAI.TamingCompatibility.HodgeStarGeometry.combine_star_frame line 66
  13. lemma OAI.TamingCompatibility.HodgeStarGeometry.combineThree_extDeriv line 88
  14. lemma OAI.TamingCompatibility.HodgeStarGeometry.combineThree_intertwines line 99
  15. lemma OAI.TamingCompatibility.HodgeStarGeometry.lower_intertwines line 110
  16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.geometric_lower_intertwines line 139