OAI/Geometry/TamingCompatibility/DifferentialForms/Form.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.MetricForms.Form line 31
  2. def OAI.TamingCompatibility.MetricForms.pairing line 34
  3. lemma OAI.TamingCompatibility.MetricForms.pairing_symm line 38
  4. lemma OAI.TamingCompatibility.MetricForms.pairing_self_nonneg line 41
  5. lemma OAI.TamingCompatibility.MetricForms.pairing_self_eq_zero line 44
  6. def OAI.TamingCompatibility.MetricForms.basisOfFrame line 58
  7. lemma OAI.TamingCompatibility.MetricForms.basisOfFrame_apply line 67
  8. lemma OAI.TamingCompatibility.MetricForms.pairing_two_eq_sum line 72
  9. lemma OAI.TamingCompatibility.MetricForms.pairing_three_eq_sum line 81
  10. def OAI.TamingCompatibility.MetricForms.isometryEquiv line 90
  11. lemma OAI.TamingCompatibility.MetricForms.isometryEquiv_apply line 95
  12. lemma OAI.TamingCompatibility.MetricForms.comp_two line 100
  13. lemma OAI.TamingCompatibility.MetricForms.pairing_two_comp line 107
  14. lemma OAI.TamingCompatibility.MetricForms.pairing_three_comp line 119
  15. lemma OAI.TamingCompatibility.HermitianHodge.pairing_coords line 137
  16. def OAI.TamingCompatibility.HermitianHodge.star line 144
  17. lemma OAI.TamingCompatibility.HermitianHodge.coords_sub line 148
  18. lemma OAI.TamingCompatibility.HermitianHodge.unitary_star_formula line 153
  19. lemma OAI.TamingCompatibility.HermitianHodge.coords_jAction line 167
  20. lemma OAI.TamingCompatibility.HermitianHodge.coords_fundamental line 185
  21. lemma OAI.TamingCompatibility.HermitianHodge.pairing_fundamental line 191
  22. lemma OAI.TamingCompatibility.HermitianHodge.coords_star line 197
  23. lemma OAI.TamingCompatibility.HermitianHodge.star_square line 210
  24. lemma OAI.TamingCompatibility.HermitianHodge.star_self_adjoint line 216
  25. lemma OAI.TamingCompatibility.HermitianHodge.star_isometry line 222
  26. lemma OAI.TamingCompatibility.HermitianHodge.star_antiInvariant line 226
  27. lemma OAI.TamingCompatibility.HermitianHodge.star_fundamental line 234
  28. lemma OAI.TamingCompatibility.HermitianHodge.fundamental_sq line 240