OAI/Algebra/AuslanderReiten/Algebras/BaseAlgebra.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.ArExplicit.Letter line 13
  2. instance OAI.ArExplicit.(instance at line 17) line 17
  3. theorem OAI.ArExplicit.Letter.card line 21
  4. structure OAI.ArExplicit.BaseAlgebra line 24
  5. def OAI.ArExplicit.BaseAlgebra.coordinates line 31
  6. instance OAI.ArExplicit.BaseAlgebra.(instance at line 37) line 37
  7. def OAI.ArExplicit.BaseAlgebra.coordinateAddEquiv line 42
  8. instance OAI.ArExplicit.BaseAlgebra.(instance at line 46) line 46
  9. theorem OAI.ArExplicit.BaseAlgebra.coeff_zero line 48
  10. theorem OAI.ArExplicit.BaseAlgebra.coeff_add line 49
  11. theorem OAI.ArExplicit.BaseAlgebra.coeff_neg line 51
  12. theorem OAI.ArExplicit.BaseAlgebra.coeff_smul line 53
  13. def OAI.ArExplicit.BaseAlgebra.product line 58
  14. instance OAI.ArExplicit.BaseAlgebra.(instance at line 74) line 74
  15. instance OAI.ArExplicit.BaseAlgebra.(instance at line 75) line 75
  16. theorem OAI.ArExplicit.BaseAlgebra.coeff_mul line 77
  17. theorem OAI.ArExplicit.BaseAlgebra.coeff_one line 79
  18. theorem OAI.ArExplicit.BaseAlgebra.product_assoc line 82
  19. instance OAI.ArExplicit.BaseAlgebra.(instance at line 86) line 86
  20. instance OAI.ArExplicit.BaseAlgebra.(instance at line 100) line 100
  21. def OAI.ArExplicit.BaseAlgebra.basisVector line 105
  22. theorem OAI.ArExplicit.BaseAlgebra.coeff_basisVector line 107
  23. theorem OAI.ArExplicit.BaseAlgebra.one_eq_vertices line 111
  24. def OAI.ArExplicit.BaseAlgebra.multiplicationTable line 115
  25. theorem OAI.ArExplicit.BaseAlgebra.basis_e_mul line 150
  26. theorem OAI.ArExplicit.BaseAlgebra.basis_x_mul line 155
  27. theorem OAI.ArExplicit.BaseAlgebra.basis_y_mul line 160
  28. theorem OAI.ArExplicit.BaseAlgebra.basis_z_mul line 165
  29. theorem OAI.ArExplicit.BaseAlgebra.basis_u_mul line 170
  30. theorem OAI.ArExplicit.BaseAlgebra.basis_v_mul line 175
  31. theorem OAI.ArExplicit.BaseAlgebra.basis_t_mul line 180
  32. theorem OAI.ArExplicit.BaseAlgebra.basis_j_mul line 185
  33. theorem OAI.ArExplicit.BaseAlgebra.basis_f_mul line 190
  34. theorem OAI.ArExplicit.BaseAlgebra.basis_n_mul line 195
  35. theorem OAI.ArExplicit.BaseAlgebra.basis_mul line 200
  36. theorem OAI.ArExplicit.BaseAlgebra.fourfold_product line 214
  37. def OAI.ArExplicit.BaseAlgebra.mapScalars line 221
  38. theorem OAI.ArExplicit.BaseAlgebra.coeff_mapScalars line 231
  39. theorem OAI.ArExplicit.BaseAlgebra.mapScalars_injective line 235
  40. def OAI.ArExplicit.BaseAlgebra.coordinateLinearEquiv line 242
  41. instance OAI.ArExplicit.BaseAlgebra.(instance at line 245) line 245
  42. theorem OAI.ArExplicit.BaseAlgebra.finrank_eq_ten line 248
  43. theorem OAI.ArExplicit.BaseAlgebra.fourfold_product_ne_zero line 252