OAI/Geometry/TamingCompatibility/Elliptic/NormalSystem.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.LocalMatrixOperator.frameVector line 13
2. lemma OAI.TamingCompatibility.LocalMatrixOperator.frameVector_apply line 16
3. def OAI.TamingCompatibility.LocalMatrixOperator.frameCovector line 19
4. def OAI.TamingCompatibility.LocalMatrixOperator.normalPrincipal line 21
5. def OAI.TamingCompatibility.LocalMatrixOperator.normalLower line 24
6. lemma OAI.TamingCompatibility.LocalMatrixOperator.frameVector_pairing line 28
7. lemma OAI.TamingCompatibility.LocalMatrixOperator.normal_operator_expansion line 35