OAI/Algebra/AuslanderReiten/Algebras/SimpleModule.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.Resolution.F_coeff_zero line 18
  2. theorem OAI.ArExplicit.Resolution.F_coeff_e line 23
  3. theorem OAI.ArExplicit.Resolution.F_coeff_x line 24
  4. theorem OAI.ArExplicit.Resolution.F_coeff_y line 25
  5. theorem OAI.ArExplicit.Resolution.F_coeff_z line 26
  6. theorem OAI.ArExplicit.Resolution.F_coeff_t line 27
  7. theorem OAI.ArExplicit.Resolution.F_coeff_j line 28
  8. theorem OAI.ArExplicit.Resolution.F_expand line 30
  9. def OAI.ArExplicit.Resolution.uPreimage line 36
  10. theorem OAI.ArExplicit.Resolution.uPreimage_spec line 41
  11. theorem OAI.ArExplicit.Resolution.mem_range_dU_iff line 48
  12. def OAI.ArExplicit.Resolution.fCoordinate line 59
  13. def OAI.ArExplicit.Resolution.simpleCoordinate line 64
  14. theorem OAI.ArExplicit.Resolution.simpleCoordinate_mk line 70
  15. theorem OAI.ArExplicit.Resolution.simpleCoordinate_eq_zero_iff line 73
  16. theorem OAI.ArExplicit.Resolution.simpleCoordinate_injective line 80
  17. def OAI.ArExplicit.Resolution.vertexF line 86
  18. theorem OAI.ArExplicit.Resolution.simpleCoordinate_surjective line 90
  19. def OAI.ArExplicit.Resolution.simpleCoordinateEquiv line 95
  20. theorem OAI.ArExplicit.Resolution.simple_finrank line 99
  21. theorem OAI.ArExplicit.Resolution.simpleCoordinate_smul line 103
  22. theorem OAI.ArExplicit.Resolution.e_smul_simple line 109
  23. theorem OAI.ArExplicit.Resolution.f_smul_simple line 114
  24. def OAI.ArExplicit.Resolution.vertexE line 119
  25. theorem OAI.ArExplicit.Resolution.e_smul_vertexE line 123
  26. theorem OAI.ArExplicit.Resolution.smul_vertexE line 127
  27. theorem OAI.ArExplicit.Resolution.hom_E_simple_eq_zero line 131
  28. theorem OAI.ArExplicit.Resolution.simple_positiveExt line 145