OAI/Geometry/TamingCompatibility/DifferentialForms/FramePairing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.AntiInvariantFrame.pairing_combination line 17
2. lemma OAI.TamingCompatibility.GeometricChart.localizedPairing_scalars line 38
3. lemma OAI.TamingCompatibility.AntiInvariantFrame.star_wedge_combination line 66
4. lemma OAI.TamingCompatibility.AntiInvariantFrame.star_wedge_anti line 85
5. def OAI.TamingCompatibility.ManifoldForms.scalarDifferential line 107
6. lemma OAI.TamingCompatibility.ManifoldForms.pullback_scalarDifferential line 111
7. lemma OAI.TamingCompatibility.ManifoldForms.scalarDifferential_smooth line 121
8. lemma OAI.TamingCompatibility.ManifoldForms.mfderiv_inverseChart_self line 131
9. lemma OAI.TamingCompatibility.ManifoldForms.exteriorDerivative_fun_smul line 140