OAI/Algebra/MarkedTensor/PolynomialAdjoint.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Nine polynomial conjugators spanning every adjoint-coordinate endomorphism.

  1. abbrev OAI.MarkedTensor.Adjoint.Mat₂ line 17
  2. abbrev OAI.MarkedTensor.Adjoint.Mat₃ line 18
  3. abbrev OAI.MarkedTensor.Adjoint.Vec₃ line 19
  4. abbrev OAI.MarkedTensor.Adjoint.mat line 21
  5. def OAI.MarkedTensor.Adjoint.traceless line 24
  6. def OAI.MarkedTensor.Adjoint.extract line 26
  7. def OAI.MarkedTensor.Adjoint.tracelessLM line 28
  8. def OAI.MarkedTensor.Adjoint.extractLM line 33
  9. def OAI.MarkedTensor.Adjoint.conjugationLM line 38
  10. def OAI.MarkedTensor.Adjoint.adjoint line 44
  11. lemma OAI.MarkedTensor.Adjoint.traceless_extract line 47
  12. lemma OAI.MarkedTensor.Adjoint.extract_traceless line 50
  13. lemma OAI.MarkedTensor.Adjoint.traceless_adjoint line 56
  14. def OAI.MarkedTensor.Adjoint.conjugator line 67
  15. lemma OAI.MarkedTensor.Adjoint.conjugator_inv line 70
  16. def OAI.MarkedTensor.Adjoint.adjointMatrix line 78
  17. lemma OAI.MarkedTensor.Adjoint.toMatrix_adjoint line 83
  18. def OAI.MarkedTensor.Adjoint.coefficient line 94
  19. lemma OAI.MarkedTensor.Adjoint.coefficient00 line 101
  20. lemma OAI.MarkedTensor.Adjoint.coefficient01 line 102
  21. lemma OAI.MarkedTensor.Adjoint.coefficient02 line 104
  22. lemma OAI.MarkedTensor.Adjoint.coefficient10 line 106
  23. lemma OAI.MarkedTensor.Adjoint.coefficient11 line 108
  24. lemma OAI.MarkedTensor.Adjoint.coefficient12 line 110
  25. lemma OAI.MarkedTensor.Adjoint.coefficient20 line 112
  26. lemma OAI.MarkedTensor.Adjoint.coefficient21 line 114
  27. lemma OAI.MarkedTensor.Adjoint.coefficient22 line 116
  28. def OAI.MarkedTensor.Adjoint.quadratic line 119
  29. lemma OAI.MarkedTensor.Adjoint.quadratic_coefficients_mem line 122
  30. def OAI.MarkedTensor.Adjoint.rowPolynomial line 143
  31. lemma OAI.MarkedTensor.Adjoint.expansion line 146
  32. lemma OAI.MarkedTensor.Adjoint.coefficients_mem line 153
  33. lemma OAI.MarkedTensor.Adjoint.span_eq_top_of_coefficients line 177
  34. lemma OAI.MarkedTensor.Adjoint.nine_matrix_span line 216
  35. theorem OAI.MarkedTensor.Adjoint.vertex_adjoint_span line 226