OAI/Algebra/AuslanderReiten/Tensor/BalancedTensorLeftExact.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.BalancedTensor.mapLeft line 15
  2. theorem OAI.ArExplicit.BalancedTensor.mapLeft_tmul line 19
  3. theorem OAI.ArExplicit.BalancedTensor.mapLeft_comp line 23
  4. theorem OAI.ArExplicit.BalancedTensor.mapLeft_zero line 30
  5. def OAI.ArExplicit.BalancedTensor.leftCoefficients line 37
  6. theorem OAI.ArExplicit.BalancedTensor.leftCoefficients_tmul line 59
  7. def OAI.ArExplicit.BalancedTensor.leftRecombine line 62
  8. theorem OAI.ArExplicit.BalancedTensor.leftRecombine_apply line 67
  9. theorem OAI.ArExplicit.BalancedTensor.leftRecombine_leftCoefficients line 71
  10. theorem OAI.ArExplicit.BalancedTensor.leftCoefficients_natural line 97
  11. theorem OAI.ArExplicit.BalancedTensor.leftRecombine_natural line 106
  12. theorem OAI.ArExplicit.BalancedTensor.mapLeft_exact line 110
  13. theorem OAI.ArExplicit.BalancedTensor.mapLeft_surjective line 134
  14. theorem OAI.ArExplicit.BalancedTensor.mapLeft_injective line 139