OAI/Algebra/Finitistic/Ordinary/OrdinarySingleTensorTerms.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SingleBimoduleTensor.complex line 18
  2. def OAI.LittleFinitistic.SingleBimoduleTensor.zeroCoefficientEquiv line 24
  3. theorem OAI.LittleFinitistic.SingleBimoduleTensor.zeroCoefficientEquiv_left line 28
  4. def OAI.LittleFinitistic.SingleBimoduleTensor.zeroTermEquiv line 32
  5. theorem OAI.LittleFinitistic.SingleBimoduleTensor.zeroTermEquiv_map line 36
  6. theorem OAI.LittleFinitistic.SingleBimoduleTensor.otherTerm_subsingleton line 49
  7. def OAI.LittleFinitistic.SingleBimoduleTensor.coefficientEquivAt line 60
  8. theorem OAI.LittleFinitistic.SingleBimoduleTensor.coefficientEquivAt_left line 65
  9. def OAI.LittleFinitistic.SingleBimoduleTensor.termEquivAt line 71
  10. theorem OAI.LittleFinitistic.SingleBimoduleTensor.termEquivAt_map line 76
  11. abbrev OAI.LittleFinitistic.SingleBimoduleTensor.selectedTermEquiv line 88
  12. def OAI.LittleFinitistic.SingleBimoduleTensor.totalTermEquiv line 90