OAI/Algebra/AuslanderReiten/Resolutions/Resolution.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.Resolution.fixedRight line 16
  2. def OAI.ArExplicit.Resolution.rightMultiply line 28
  3. def OAI.ArExplicit.Resolution.projection line 33
  4. theorem OAI.ArExplicit.Resolution.projection_surjective line 38
  5. theorem OAI.ArExplicit.Resolution.projective_fixedRight line 43
  6. theorem OAI.ArExplicit.Resolution.finite_fixedRight line 50
  7. abbrev OAI.ArExplicit.Resolution.E line 55
  8. abbrev OAI.ArExplicit.Resolution.F line 57
  9. instance OAI.ArExplicit.Resolution.(instance at line 59) line 59
  10. instance OAI.ArExplicit.Resolution.(instance at line 61) line 61
  11. instance OAI.ArExplicit.Resolution.(instance at line 64) line 64
  12. instance OAI.ArExplicit.Resolution.(instance at line 66) line 66
  13. def OAI.ArExplicit.Resolution.rightBetween line 69
  14. def OAI.ArExplicit.Resolution.ell line 75
  15. theorem OAI.ArExplicit.Resolution.ell_right_e line 77
  16. def OAI.ArExplicit.Resolution.dU line 80
  17. def OAI.ArExplicit.Resolution.dEll line 84
  18. theorem OAI.ArExplicit.Resolution.coe_dU line 86
  19. theorem OAI.ArExplicit.Resolution.coe_dEll line 87
  20. theorem OAI.ArExplicit.Resolution.E_coeff_zero line 89
  21. theorem OAI.ArExplicit.Resolution.E_coeff_u line 94
  22. theorem OAI.ArExplicit.Resolution.E_coeff_v line 95
  23. theorem OAI.ArExplicit.Resolution.E_coeff_f line 96
  24. theorem OAI.ArExplicit.Resolution.E_coeff_n line 97
  25. theorem OAI.ArExplicit.Resolution.E_expand line 99
  26. theorem OAI.ArExplicit.Resolution.mul_u_formula line 106
  27. theorem OAI.ArExplicit.Resolution.mul_ell_formula line 113
  28. theorem OAI.ArExplicit.Resolution.mul_u_eq_zero_iff line 124
  29. theorem OAI.ArExplicit.Resolution.mul_ell_eq_zero_iff line 139
  30. def OAI.ArExplicit.Resolution.ellPreimage line 156
  31. theorem OAI.ArExplicit.Resolution.ellPreimage_spec line 161
  32. theorem OAI.ArExplicit.Resolution.uKernel_expand line 173
  33. theorem OAI.ArExplicit.Resolution.ellKernel_expand line 181
  34. theorem OAI.ArExplicit.Resolution.ell_one_mul_u line 190
  35. theorem OAI.ArExplicit.Resolution.ell_successor_mul line 194
  36. theorem OAI.ArExplicit.Resolution.dU_comp_dEll_one line 198
  37. theorem OAI.ArExplicit.Resolution.dEll_comp_successor line 205
  38. theorem OAI.ArExplicit.Resolution.exact_dU line 212
  39. theorem OAI.ArExplicit.Resolution.exact_dEll line 226