OAI/Geometry/TamingCompatibility/DifferentialForms/RadialScalarOff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TamingCompatibility.GeometricHilbert.closedLift_scalar_off_source line 39
2. def OAI.TamingCompatibility.supportedSchwartz line 95
3. lemma OAI.TamingCompatibility.supportedSchwartz_compact line 105
4. lemma OAI.TamingCompatibility.ManifoldForms.chartLift_smul line 121
5. lemma OAI.TamingCompatibility.GeometricChart.coordinateTest_smul line 136
6. lemma OAI.TamingCompatibility.GeometricChart.manifoldTest_smul line 141
7. def OAI.TamingCompatibility.GeometricHilbert.scalarTestLM line 157
8. def OAI.TamingCompatibility.GeometricHilbert.smoothPullbackLM line 184
9. def OAI.TamingCompatibility.GeometricHilbert.scalarCorrectionLM line 190
10. lemma OAI.TamingCompatibility.GeometricHilbert.scalarCorrectionLM_eq line 198