OAI/Algebra/AffineCancellation/TorsorInverse.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ComplexCancellation.Torsor.KB line 11
  2. def OAI.ComplexCancellation.Torsor.ib line 12
  3. def OAI.ComplexCancellation.Torsor.bc line 13
  4. lemma OAI.ComplexCancellation.Torsor.compatibility line 16
  5. lemma OAI.ComplexCancellation.Torsor.back_ab line 22
  6. lemma OAI.ComplexCancellation.Torsor.back_dc line 25
  7. lemma OAI.ComplexCancellation.Torsor.back_db line 28
  8. lemma OAI.ComplexCancellation.Torsor.bc_det line 32
  9. lemma OAI.ComplexCancellation.Torsor.back_ac line 34
  10. def OAI.ComplexCancellation.Torsor.w line 40
  11. def OAI.ComplexCancellation.Torsor.wi line 41
  12. lemma OAI.ComplexCancellation.Torsor.back_a line 42
  13. lemma OAI.ComplexCancellation.Torsor.back_d line 46
  14. lemma OAI.ComplexCancellation.Torsor.back_b line 50
  15. lemma OAI.ComplexCancellation.Torsor.back_c line 54
  16. lemma OAI.ComplexCancellation.Torsor.w_wi line 58
  17. def OAI.ComplexCancellation.Torsor.W line 61
  18. def OAI.ComplexCancellation.Torsor.backward line 62
  19. lemma OAI.ComplexCancellation.Torsor.backward_C line 68
  20. lemma OAI.ComplexCancellation.Torsor.backward_T_one line 69
  21. lemma OAI.ComplexCancellation.Torsor.backward_T_neg_one line 73
  22. lemma OAI.ComplexCancellation.Torsor.backward_frameMap line 78
  23. lemma OAI.ComplexCancellation.Torsor.backward_forward_j line 94
  24. lemma OAI.ComplexCancellation.Torsor.backward_forward_τ line 97
  25. lemma OAI.ComplexCancellation.Torsor.backward_forward_V line 105
  26. lemma OAI.ComplexCancellation.Torsor.backward_forward line 113
  27. lemma OAI.ComplexCancellation.Torsor.forward_injective line 122