OAI/RingTheory/BassTrace/ClosedPaths.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BassTrace.Paths.GroupMatrix line 18
  2. abbrev OAI.BassTrace.Paths.ScalarMatrix line 20
  3. def OAI.BassTrace.Paths.coefficient line 22
  4. def OAI.BassTrace.Paths.support line 25
  5. lemma OAI.BassTrace.Paths.mem_support line 30
  6. lemma OAI.BassTrace.Paths.entry_support_subset line 46
  7. lemma OAI.BassTrace.Paths.coefficient_mul line 53
  8. def OAI.BassTrace.Paths.kernel line 67
  9. lemma OAI.BassTrace.Paths.kernel_left_invariant line 71
  10. lemma OAI.BassTrace.Paths.kernel_row_finite line 75
  11. lemma OAI.BassTrace.Paths.kernel_column_finite line 83
  12. lemma OAI.BassTrace.Paths.kernel_idempotent line 91
  13. lemma OAI.BassTrace.Paths.kernel_idempotent_finsum line 97
  14. def OAI.BassTrace.Paths.pathSetoid line 118
  15. abbrev OAI.BassTrace.Paths.Orbit line 131
  16. def OAI.BassTrace.Paths.increment line 133
  17. lemma OAI.BassTrace.Paths.increment_castSucc line 136
  18. lemma OAI.BassTrace.Paths.increment_last line 140
  19. lemma OAI.BassTrace.Paths.increment_invariant line 144
  20. lemma OAI.BassTrace.Paths.increment_eq_imp_related line 155
  21. def OAI.BassTrace.Paths.orbitIncrement line 175
  22. lemma OAI.BassTrace.Paths.orbitIncrement_injective line 181
  23. def OAI.BassTrace.Paths.weight line 190
  24. lemma OAI.BassTrace.Paths.weight_invariant line 195
  25. lemma OAI.BassTrace.Paths.weight_ne_zero_support line 201
  26. def OAI.BassTrace.Paths.orbitWeight line 213
  27. lemma OAI.BassTrace.Paths.orbitWeight_finite line 219
  28. def OAI.BassTrace.Paths.pathVector line 229
  29. def OAI.BassTrace.Paths.twist line 238
  30. lemma OAI.BassTrace.Paths.twist_castSucc line 241
  31. lemma OAI.BassTrace.Paths.twist_last line 244
  32. lemma OAI.BassTrace.Paths.rotate_castSucc line 247
  33. lemma OAI.BassTrace.Paths.increment_twist line 250
  34. lemma OAI.BassTrace.Paths.weight_twist line 280
  35. def OAI.BassTrace.Paths.prefixProduct line 292
  36. lemma OAI.BassTrace.Paths.weight_eq_prefix line 297
  37. lemma OAI.BassTrace.Paths.prefixProduct_snoc line 304
  38. lemma OAI.BassTrace.Paths.weight_snoc line 316
  39. lemma OAI.BassTrace.Paths.weight_snoc_finite line 325
  40. lemma OAI.BassTrace.Paths.weight_snoc_finsum line 333