OAI/Algebra/AuslanderReiten/Tensor/BalancedTensor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.balancingRelations line 16
  2. abbrev OAI.ArExplicit.BalancedTensor line 20
  3. def OAI.ArExplicit.BalancedTensor.tmul line 26
  4. theorem OAI.ArExplicit.BalancedTensor.zero_tmul line 29
  5. theorem OAI.ArExplicit.BalancedTensor.tmul_zero line 32
  6. theorem OAI.ArExplicit.BalancedTensor.add_tmul line 35
  7. theorem OAI.ArExplicit.BalancedTensor.tmul_add line 38
  8. theorem OAI.ArExplicit.BalancedTensor.scalar_tmul line 41
  9. theorem OAI.ArExplicit.BalancedTensor.tmul_scalar line 45
  10. theorem OAI.ArExplicit.BalancedTensor.balance line 48
  11. def OAI.ArExplicit.BalancedTensor.mk line 53
  12. def OAI.ArExplicit.BalancedTensor.lift line 63
  13. theorem OAI.ArExplicit.BalancedTensor.lift_tmul line 72
  14. theorem OAI.ArExplicit.BalancedTensor.hom_ext line 76