OAI/Algebra/MarkedTensor/AdjointCoordinates.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Traceless matrix coordinates, adjoint actions and base change of spanning families.

  1. abbrev OAI.BoundaryOnly.Holonomy.Mat₂ line 16
  2. abbrev OAI.BoundaryOnly.Holonomy.Vec₃ line 17
  3. def OAI.BoundaryOnly.Holonomy.half line 19
  4. lemma OAI.BoundaryOnly.Holonomy.two_half line 20
  5. def OAI.BoundaryOnly.Holonomy.traceless line 23
  6. def OAI.BoundaryOnly.Holonomy.coordinates line 24
  7. def OAI.BoundaryOnly.Holonomy.extract line 27
  8. lemma OAI.BoundaryOnly.Holonomy.scalar_lie line 29
  9. lemma OAI.BoundaryOnly.Holonomy.scalar_lie_left line 35
  10. lemma OAI.BoundaryOnly.Holonomy.traceless_coordinates line 39
  11. lemma OAI.BoundaryOnly.Holonomy.traceless_extract line 48
  12. lemma OAI.BoundaryOnly.Holonomy.extract_traceless line 51
  13. def OAI.BoundaryOnly.Holonomy.tracelessLM line 57
  14. def OAI.BoundaryOnly.Holonomy.extractLM line 62
  15. def OAI.BoundaryOnly.Holonomy.conjugationLM line 67
  16. def OAI.BoundaryOnly.Holonomy.adjoint line 72
  17. lemma OAI.BoundaryOnly.Holonomy.traceless_adjoint line 75
  18. lemma OAI.BoundaryOnly.Holonomy.conjugate_scalar line 83
  19. lemma OAI.BoundaryOnly.Holonomy.reference_traceless_triple line 96
  20. lemma OAI.BoundaryOnly.Holonomy.matrix_span_base_change line 118
  21. lemma OAI.BoundaryOnly.Holonomy.adjoint_matrix_map line 146
  22. lemma OAI.BoundaryOnly.Holonomy.adjoint_span_base_change line 163