OAI/Algebra/AuslanderReiten/Algebras/TrivialExtension.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ArExplicit.TrivialExtension line 13
  2. def OAI.ArExplicit.TrivialExtension.coordinates line 21
  3. instance OAI.ArExplicit.TrivialExtension.(instance at line 27) line 27
  4. instance OAI.ArExplicit.TrivialExtension.(instance at line 28) line 28
  5. theorem OAI.ArExplicit.TrivialExtension.base_zero line 30
  6. theorem OAI.ArExplicit.TrivialExtension.dual_zero line 31
  7. theorem OAI.ArExplicit.TrivialExtension.base_add line 32
  8. theorem OAI.ArExplicit.TrivialExtension.dual_add line 33
  9. theorem OAI.ArExplicit.TrivialExtension.base_smul line 34
  10. theorem OAI.ArExplicit.TrivialExtension.dual_smul line 35
  11. def OAI.ArExplicit.TrivialExtension.leftDual line 37
  12. def OAI.ArExplicit.TrivialExtension.rightDual line 42
  13. theorem OAI.ArExplicit.TrivialExtension.leftDual_apply line 47
  14. theorem OAI.ArExplicit.TrivialExtension.rightDual_apply line 49
  15. def OAI.ArExplicit.TrivialExtension.product line 52
  16. instance OAI.ArExplicit.TrivialExtension.(instance at line 55) line 55
  17. instance OAI.ArExplicit.TrivialExtension.(instance at line 56) line 56
  18. theorem OAI.ArExplicit.TrivialExtension.base_one line 58
  19. theorem OAI.ArExplicit.TrivialExtension.dual_one line 59
  20. theorem OAI.ArExplicit.TrivialExtension.base_mul line 60
  21. theorem OAI.ArExplicit.TrivialExtension.dual_mul_apply line 61
  22. instance OAI.ArExplicit.TrivialExtension.(instance at line 64) line 64
  23. instance OAI.ArExplicit.TrivialExtension.(instance at line 96) line 96
  24. def OAI.ArExplicit.TrivialExtension.inl line 109
  25. def OAI.ArExplicit.TrivialExtension.inr line 111
  26. def OAI.ArExplicit.TrivialExtension.inlHom line 113
  27. theorem OAI.ArExplicit.TrivialExtension.inlHom_injective line 131
  28. theorem OAI.ArExplicit.TrivialExtension.inr_mul_inr line 135
  29. def OAI.ArExplicit.TrivialExtension.trace line 141
  30. theorem OAI.ArExplicit.TrivialExtension.trace_apply line 146
  31. theorem OAI.ArExplicit.TrivialExtension.trace_mul line 148
  32. theorem OAI.ArExplicit.TrivialExtension.trace_mul_comm line 151
  33. def OAI.ArExplicit.TrivialExtension.traceForm line 154
  34. theorem OAI.ArExplicit.TrivialExtension.traceForm_apply line 162
  35. theorem OAI.ArExplicit.TrivialExtension.traceForm_symmetric line 165
  36. theorem OAI.ArExplicit.TrivialExtension.traceForm_associative line 168
  37. def OAI.ArExplicit.TrivialExtension.coordinateLinearEquiv line 171
  38. theorem OAI.ArExplicit.TrivialExtension.traceForm_nondegenerate line 180
  39. instance OAI.ArExplicit.TrivialExtension.(instance at line 200) line 200
  40. theorem OAI.ArExplicit.TrivialExtension.finrank_eq_twice line 203
  41. abbrev OAI.ArExplicit.T line 211
  42. theorem OAI.ArExplicit.T_finrank line 213
  43. def OAI.ArExplicit.T.coordinateFunctional line 220
  44. def OAI.ArExplicit.T.lower line 225
  45. def OAI.ArExplicit.T.upper line 227
  46. theorem OAI.ArExplicit.T.trace_lower_upper line 229
  47. theorem OAI.ArExplicit.T.trace_upper_lower line 235
  48. theorem OAI.ArExplicit.T.upper_mul_upper line 240