OAI/Geometry/TamingCompatibility/DifferentialForms/FormPairing.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.FormMetric.sharp line 24
  2. lemma OAI.TamingCompatibility.FormMetric.sharp_inner line 30
  3. lemma OAI.TamingCompatibility.FormMetric.sharp_injective line 34
  4. def OAI.TamingCompatibility.FormMetric.pairing line 39
  5. lemma OAI.TamingCompatibility.FormMetric.pairing_symm line 41
  6. lemma OAI.TamingCompatibility.FormMetric.pairing_self_nonneg line 44
  7. lemma OAI.TamingCompatibility.FormMetric.pairing_self_eq_zero line 47
  8. def OAI.TamingCompatibility.FormMetric.pairLeft line 51
  9. def OAI.TamingCompatibility.FormMetric.pairRight line 52
  10. def OAI.TamingCompatibility.FormMetric.wedgeFamily line 54
  11. lemma OAI.TamingCompatibility.FormMetric.wedgeFamily_orthonormal line 57
  12. def OAI.TamingCompatibility.FormMetric.wedgeBasis line 66
  13. lemma OAI.TamingCompatibility.FormMetric.wedgeBasis_apply line 73
  14. lemma OAI.TamingCompatibility.FormMetric.wedgeBasis_repr line 77
  15. lemma OAI.TamingCompatibility.FormMetric.pairing_eq_sum line 83
  16. instance OAI.TamingCompatibility.FormMetric.formFiniteDimensional line 101
  17. def OAI.TamingCompatibility.FormMetric.sharpCLM line 104
  18. def OAI.TamingCompatibility.FormMetric.pairingCLM line 107
  19. lemma OAI.TamingCompatibility.FormMetric.pairingCLM_apply line 110
  20. lemma OAI.TamingCompatibility.FormMetric.pairing_add_left line 112
  21. lemma OAI.TamingCompatibility.FormMetric.pairing_smul_left line 116
  22. lemma OAI.TamingCompatibility.FormMetric.pairing_add_right line 120
  23. lemma OAI.TamingCompatibility.FormMetric.pairing_smul_right line 124
  24. lemma OAI.TamingCompatibility.FormMetric.pairing_sub_left line 128
  25. lemma OAI.TamingCompatibility.FormMetric.pairing_sub_right line 132
  26. lemma OAI.TamingCompatibility.FormMetric.contDiff_pairing line 136
  27. def OAI.TamingCompatibility.FormMetric.tripleIndices line 143
  28. def OAI.TamingCompatibility.FormMetric.tripleFamily line 145
  29. lemma OAI.TamingCompatibility.FormMetric.tripleFamily_orthonormal line 148
  30. def OAI.TamingCompatibility.FormMetric.tripleBasis line 156
  31. lemma OAI.TamingCompatibility.FormMetric.tripleBasis_repr line 163
  32. lemma OAI.TamingCompatibility.FormMetric.pairing_three line 170