OAI/Algebra/AffineCancellation/TorsorFrame.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ComplexCancellation.Torsor.Frame line 13
  2. abbrev OAI.ComplexCancellation.Torsor.L line 23
  3. def OAI.ComplexCancellation.Torsor.cc line 24
  4. def OAI.ComplexCancellation.Torsor.base line 25
  5. lemma OAI.ComplexCancellation.Torsor.mono_pair line 27
  6. def OAI.ComplexCancellation.Torsor.frameEval line 31
  7. lemma OAI.ComplexCancellation.Torsor.frameEval_relation line 33
  8. def OAI.ComplexCancellation.Torsor.frameMap line 37
  9. lemma OAI.ComplexCancellation.Torsor.frameMap_π line 42
  10. lemma OAI.ComplexCancellation.Torsor.frameMap_a line 44
  11. lemma OAI.ComplexCancellation.Torsor.frameMap_d line 45
  12. lemma OAI.ComplexCancellation.Torsor.frameMap_b line 46
  13. lemma OAI.ComplexCancellation.Torsor.frameMap_c line 47
  14. lemma OAI.ComplexCancellation.Torsor.frameMap_u line 48
  15. lemma OAI.ComplexCancellation.Torsor.frameMap_inclusion line 49
  16. lemma OAI.ComplexCancellation.Torsor.frame_f line 66
  17. lemma OAI.ComplexCancellation.Torsor.frame_g line 70
  18. def OAI.ComplexCancellation.Torsor.vb line 75
  19. lemma OAI.ComplexCancellation.Torsor.vb_equation line 76
  20. def OAI.ComplexCancellation.Torsor.forwardEval line 83
  21. lemma OAI.ComplexCancellation.Torsor.forwardEval_C line 89
  22. lemma OAI.ComplexCancellation.Torsor.forwardEval_X line 90
  23. lemma OAI.ComplexCancellation.Torsor.forwardEval_rel line 93
  24. def OAI.ComplexCancellation.Torsor.forward line 96
  25. lemma OAI.ComplexCancellation.Torsor.forward_π line 101
  26. lemma OAI.ComplexCancellation.Torsor.forward_j line 104
  27. lemma OAI.ComplexCancellation.Torsor.forward_τ line 108
  28. lemma OAI.ComplexCancellation.Torsor.forward_V line 110
  29. lemma OAI.ComplexCancellation.Torsor.base_p_ne_zero line 112
  30. lemma OAI.ComplexCancellation.Torsor.forward_pullback line 121