OAI/RingTheory/BassTrace/MatrixK0.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.K0.trace_reindex line 18

    Also declared: ComparatorChallenges/BassTorsionFree.lean:155 (same declaration text).

  2. lemma OAI.BassTrace.K0.trace_directSum line 24

    Also declared: ComparatorChallenges/BassTorsionFree.lean:161 (same declaration text).

  3. lemma OAI.BassTrace.K0.relations_in_kernel line 31

    Also declared: ComparatorChallenges/BassTorsionFree.lean:168 (same declaration text).

  4. def OAI.BassTrace.K0.hsCoefficient line 44

    Also declared: ComparatorChallenges/BassTorsionFree.lean:181 (same declaration text).

  5. lemma OAI.BassTrace.K0.hsCoefficient_classOf line 47
  6. lemma OAI.BassTrace.K0.classTrace_apply line 59
  7. lemma OAI.BassTrace.K0.rawTrace_apply line 65
  8. lemma OAI.BassTrace.K0.relations_in_trace_kernel line 75
  9. lemma OAI.BassTrace.K0.HattoriStallings_apply line 83
  10. lemma OAI.BassTrace.K0.HattoriStallings_classOf line 88
  11. theorem OAI.BassTrace.K0.bassTraceK0 line 98
  12. theorem OAI.BassTrace.K0.bassTraceK0_support line 112