OAI/Geometry/TamingCompatibility/DifferentialForms/FunSmul.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ManifoldForms.Smooth.fun_smul line 32
2. lemma OAI.TamingCompatibility.ManifoldForms.exteriorDerivative_eq_zero_of_eventually line 39
3. lemma OAI.TamingCompatibility.ManifoldForms.exteriorDerivative_fun_smul_vanishes line 55
4. lemma OAI.TamingCompatibility.EuclideanStokes.integral_directional_eq_zero line 70
5. lemma OAI.TamingCompatibility.EuclideanStokes.integral_extDeriv_eq_zero line 87
6. lemma OAI.TamingCompatibility.SignedStokes.integral_extDeriv_on_open line 116
7. lemma OAI.TamingCompatibility.ManifoldStokes.coefficient_add line 167
8. lemma OAI.TamingCompatibility.ManifoldStokes.coefficient_smul line 175
9. lemma OAI.TamingCompatibility.ManifoldStokes.coefficient_integrable line 183
10. def OAI.TamingCompatibility.ManifoldStokes.integral line 190
11. lemma OAI.TamingCompatibility.ManifoldStokes.integral_exteriorDerivative_cutoff line 203
12. theorem OAI.TamingCompatibility.ManifoldStokes.stokes line 255