OAI/Geometry/TamingCompatibility/DifferentialForms/StarTwoComp.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TamingCompatibility.MetricHodge.starTwo_comp line 31
  2. lemma OAI.TamingCompatibility.MetricHodge.starThree_comp line 44
  3. lemma OAI.TamingCompatibility.MetricHodge.starTwo_self_adjoint line 72
  4. lemma OAI.TamingCompatibility.MetricHodge.starTwo_antiInvariant line 80
  5. def OAI.TamingCompatibility.ManifoldHodge.tangentMetric line 107
  6. def OAI.TamingCompatibility.ManifoldHodge.starTwo line 113
  7. def OAI.TamingCompatibility.ManifoldHodge.starThree line 116
  8. lemma OAI.TamingCompatibility.ManifoldHodge.starTwo_square line 120
  9. lemma OAI.TamingCompatibility.ManifoldHodge.starTwo_antiInvariant line 128
  10. lemma OAI.TamingCompatibility.ManifoldHodge.starThree_eq_zero line 136
  11. def OAI.TamingCompatibility.ManifoldHodge.inverseChartEquiv line 150
  12. lemma OAI.TamingCompatibility.ManifoldHodge.inverseChartEquiv_coe line 157
  13. def OAI.TamingCompatibility.ManifoldHodge.flatMetric line 162
  14. def OAI.TamingCompatibility.ManifoldHodge.coordinateMetric line 167
  15. lemma OAI.TamingCompatibility.ManifoldHodge.coordinateMetric_bilinear line 174
  16. lemma OAI.TamingCompatibility.ManifoldHodge.coordinateMetric_pullback line 179
  17. def OAI.TamingCompatibility.ManifoldHodge.coordinateJ line 190
  18. lemma OAI.TamingCompatibility.ManifoldHodge.coordinateJ_conjugate line 195
  19. lemma OAI.TamingCompatibility.ManifoldHodge.coordinateJ_intertwine line 208
  20. lemma OAI.TamingCompatibility.ManifoldHodge.coordinateJ_square line 214
  21. lemma OAI.TamingCompatibility.ManifoldHodge.coordinateMetric_hermitian line 219
  22. lemma OAI.TamingCompatibility.ManifoldHodge.pullback_starTwo line 227
  23. lemma OAI.TamingCompatibility.ManifoldHodge.pullback_starThree line 242
  24. lemma OAI.TamingCompatibility.ManifoldHodge.coordinateMetric_smooth line 255
  25. lemma OAI.TamingCompatibility.ManifoldHodge.coordinateJ_smooth line 262
  26. lemma OAI.TamingCompatibility.ManifoldHodge.starTwo_smooth line 266
  27. lemma OAI.TamingCompatibility.ManifoldHodge.starThree_smooth line 280
  28. def OAI.TamingCompatibility.ManifoldHodge.codifferential line 294
  29. lemma OAI.TamingCompatibility.ManifoldHodge.coclosed_selfdual_closed line 298
  30. lemma OAI.TamingCompatibility.ManifoldHodge.coclosed_antiInvariant_closed line 305