OAI/Geometry/TamingCompatibility/DifferentialForms/MetricOperatorInner.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.metricOperator_inner line 13
2. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.cometric_eq_frame line 17
3. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.frameMap_adjoint_basis line 47
4. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.principal_eq_frame line 57
5. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.principal_pullback_frame line 67