OAI/Geometry/TamingCompatibility/DifferentialForms/ComplexReal.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.ComplexMatrix.retract line 17
  2. lemma OAI.TamingCompatibility.ComplexMatrix.retract_apply line 21
  3. lemma OAI.TamingCompatibility.ComplexMatrix.retract_embed line 22
  4. def OAI.TamingCompatibility.ComplexMatrix.entry line 29
  5. lemma OAI.TamingCompatibility.ComplexMatrix.entry_apply line 32
  6. def OAI.TamingCompatibility.ComplexMatrix.coefficient line 35
  7. lemma OAI.TamingCompatibility.ComplexMatrix.coefficient_apply line 39
  8. lemma OAI.TamingCompatibility.ComplexMatrix.real_sum_coord line 42
  9. lemma OAI.TamingCompatibility.ComplexMatrix.complex_sum_coord line 45
  10. lemma OAI.TamingCompatibility.ComplexMatrix.real_matrix_apply line 49
  11. lemma OAI.TamingCompatibility.ComplexMatrix.schwartz_matrix_embed line 58
  12. lemma OAI.TamingCompatibility.ComplexMatrix.multiply_embed line 73
  13. def OAI.TamingCompatibility.ComplexMatrix.firstOrder line 93
  14. def OAI.TamingCompatibility.ComplexMatrix.formalAdjoint line 97
  15. def OAI.TamingCompatibility.ComplexMatrix.square line 103
  16. lemma OAI.TamingCompatibility.ComplexMatrix.lineDeriv_embed line 109
  17. lemma OAI.TamingCompatibility.ComplexMatrix.distribution_lineDeriv_embed line 118
  18. lemma OAI.TamingCompatibility.ComplexMatrix.firstOrder_embed line 123
  19. lemma OAI.TamingCompatibility.ComplexMatrix.formalAdjoint_embed line 131
  20. lemma OAI.TamingCompatibility.ComplexMatrix.square_embed line 139
  21. lemma OAI.TamingCompatibility.ComplexMatrix.multiply_apply_component line 159
  22. lemma OAI.TamingCompatibility.ComplexMatrix.multiply_derivative line 166
  23. lemma OAI.TamingCompatibility.ComplexMatrix.multiply_add line 171
  24. lemma OAI.TamingCompatibility.ComplexMatrix.multiply_sum line 187
  25. lemma OAI.TamingCompatibility.ComplexMatrix.coefficient_derivative line 209
  26. def OAI.TamingCompatibility.ComplexMatrix.entryProduct line 213
  27. lemma OAI.TamingCompatibility.ComplexMatrix.entryProduct_apply line 215
  28. lemma OAI.TamingCompatibility.ComplexMatrix.entryProduct_test line 218
  29. def OAI.TamingCompatibility.ComplexMatrix.matProduct line 227
  30. lemma OAI.TamingCompatibility.ComplexMatrix.multiply_comp line 230