OAI/Algebra/AuslanderReiten/Cocycles/SparseCocycle.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.CocycleData.evalMul line 12
  2. theorem OAI.ArExplicit.CocycleData.multiplication_eq line 15
  3. theorem OAI.ArExplicit.CocycleData.linearMap_list_sum_apply line 23
  4. def OAI.ArExplicit.CocycleData.TripleMonomial.linear line 30
  5. def OAI.ArExplicit.CocycleData.evalTriple line 36
  6. theorem OAI.ArExplicit.CocycleData.TripleMonomial.linear_apply line 40
  7. def OAI.ArExplicit.CocycleData.p line 46
  8. theorem OAI.ArExplicit.CocycleData.p_apply line 49
  9. theorem OAI.ArExplicit.CocycleData.basis_evaluation line 52
  10. theorem OAI.ArExplicit.CocycleData.p_txJ line 64
  11. theorem OAI.ArExplicit.CocycleData.p_tyJ line 72
  12. theorem OAI.ArExplicit.CocycleData.p_detecting_cycle line 81