OAI/Geometry/SmoothYau/Smoothness/LinearMetricForm.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.linearMetricForm line 13
2. lemma OAI.YauCounterexamples.linearMetricForm_smooth line 16
3. def OAI.YauCounterexamples.linearPullbackMetric line 24
4. lemma OAI.YauCounterexamples.linearPullbackMetric_flat line 29
5. lemma OAI.YauCounterexamples.linearPullbackMetric_first line 34
6. lemma OAI.YauCounterexamples.linearPullbackMetric_Christoffel line 45
7. lemma OAI.YauCounterexamples.fderiv_linearEquiv_comp line 55
8. lemma OAI.YauCounterexamples.second_linearEquiv_comp line 60
9. lemma OAI.YauCounterexamples.linearPullbackMetric_hessian line 70
10. lemma OAI.YauCounterexamples.linearPullbackMetric_gradient line 77