OAI/Geometry/TamingCompatibility/Elliptic/SquarePrincipal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.ComplexMatrix.principalMatrix line 14
2. lemma OAI.TamingCompatibility.ComplexMatrix.principalMatrix_apply line 19
3. def OAI.TamingCompatibility.ComplexMatrix.principalScalar line 26
4. lemma OAI.TamingCompatibility.ComplexMatrix.entry_polarized line 30
5. lemma OAI.TamingCompatibility.ComplexMatrix.principalScalar_apply line 37
6. lemma OAI.TamingCompatibility.ComplexMatrix.principalMatrix_scalar line 48
7. lemma OAI.TamingCompatibility.ComplexMatrix.first_zero_is_matrixLower line 67
8. lemma OAI.TamingCompatibility.LocalMatrixOperator.normalSymbol_weighted_polarized line 81