OAI/Algebra/MarkedTensor/MatrixIdeals.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Matrix ideal arithmetic, conjugation errors and triple commutator congruences.

  1. lemma OAI.BoundaryOnly.Holonomy.matrix_mul_mem line 16
  2. lemma OAI.BoundaryOnly.Holonomy.matrix_mul_right line 24
  3. abbrev OAI.BoundaryOnly.Holonomy.mat line 31
  4. lemma OAI.BoundaryOnly.Holonomy.mat_mul line 33
  5. lemma OAI.BoundaryOnly.Holonomy.mat_one line 34
  6. lemma OAI.BoundaryOnly.Holonomy.inv_deviation line 36
  7. lemma OAI.BoundaryOnly.Holonomy.product_deviation line 44
  8. lemma OAI.BoundaryOnly.Holonomy.commutator_error line 55
  9. lemma OAI.BoundaryOnly.Holonomy.nested_lie_mem_four line 81
  10. abbrev OAI.BoundaryOnly.Holonomy.lie line 117
  11. lemma OAI.BoundaryOnly.Holonomy.lie_mem line 119
  12. lemma OAI.BoundaryOnly.Holonomy.inverse_difference line 125
  13. lemma OAI.BoundaryOnly.Holonomy.conjugate_deviation line 135
  14. lemma OAI.BoundaryOnly.Holonomy.conjugate_error line 139
  15. lemma OAI.BoundaryOnly.Holonomy.lie_congruence line 152
  16. lemma OAI.BoundaryOnly.Holonomy.triple_congruence line 163
  17. lemma OAI.BoundaryOnly.Holonomy.reference_triple_mem line 181