OAI/RingTheory/BassTrace/ModuleK0.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BassTrace.RightProjective.Object.presentationClass_eq line 17
2. lemma OAI.BassTrace.RightProjective.Object.presentationClass_iso line 20
3. lemma OAI.BassTrace.RightProjective.Object.presentationClass_prod line 25
4. def OAI.BassTrace.RightProjective.moduleClass line 34
5. lemma OAI.BassTrace.RightProjective.moduleRelations_in_kernel line 37
6. lemma OAI.BassTrace.RightProjective.presentation_moduleClass line 49
7. lemma OAI.BassTrace.RightProjective.HattoriStallings_moduleClass line 55
8. lemma OAI.BassTrace.RightProjective.HattoriStallings_moduleClass_coefficient line 61