OAI/Geometry/NodalSets/Charts/MetricFluxPullback.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Yau.Geometry.sourcePrincipal line 10
2. lemma OAI.Yau.Geometry.covector_basis line 14
3. lemma OAI.Yau.Geometry.inversePulledForm_covector line 23
4. lemma OAI.Yau.Geometry.principal_jacobian_sum line 35
5. lemma OAI.Yau.Geometry.adjugate_equiv_apply line 47
6. theorem OAI.Yau.Geometry.determinant_principal_jacobian line 59