OAI/Geometry/TamingCompatibility/DifferentialForms/ComplexMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.ComplexMatrix.R line 11
2. abbrev OAI.TamingCompatibility.ComplexMatrix.C line 12
3. def OAI.TamingCompatibility.ComplexMatrix.embed line 14
4. lemma OAI.TamingCompatibility.ComplexMatrix.embed_apply line 18
5. def OAI.TamingCompatibility.ComplexMatrix.unit line 20
6. lemma OAI.TamingCompatibility.ComplexMatrix.unit_apply line 24
7. def OAI.TamingCompatibility.ComplexMatrix.multiply line 30
8. lemma OAI.TamingCompatibility.ComplexMatrix.fiberMap_schwartz line 34
9. lemma OAI.TamingCompatibility.ComplexMatrix.product_schwartz line 49
10. lemma OAI.TamingCompatibility.ComplexMatrix.multiply_schwartz line 58