OAI/Geometry/TamingCompatibility/Hodge/LocalCodifferential.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.MetricForms.pairing_add_left line 17
2. lemma OAI.TamingCompatibility.MetricHodge.starThree_add line 35
3. lemma OAI.TamingCompatibility.MetricHodge.starThree_smul line 42
4. def OAI.TamingCompatibility.MetricHodge.starThreeCLM line 50
5. lemma OAI.TamingCompatibility.MetricHodge.starThreeCLM_apply line 56
6. lemma OAI.TamingCompatibility.SmoothHodge.starThreeCLM_contDiffOn line 72
7. lemma OAI.TamingCompatibility.ExteriorForms.extDeriv_variable_smul line 87
8. lemma OAI.TamingCompatibility.ManifoldHodge.pullback_codifferential_antiInvariant line 99