OAI/RingTheory/BassTrace/Definitions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BassTrace.K0.Idempotent line 19

   Also declared: ComparatorChallenges/BassTorsionFree.lean:101 (same declaration text), ComparatorChallenges/BassTrace.lean:30 (same declaration text).

2. def OAI.BassTrace.K0.directSum line 26

   Also declared: ComparatorChallenges/BassTorsionFree.lean:108 (same declaration text), ComparatorChallenges/BassTrace.lean:37 (same declaration text).

3. def OAI.BassTrace.K0.relationGenerators line 33

   Also declared: ComparatorChallenges/BassTorsionFree.lean:115 (same declaration text), ComparatorChallenges/BassTrace.lean:44 (same declaration text).

4. def OAI.BassTrace.K0.relations line 39

   Also declared: ComparatorChallenges/BassTorsionFree.lean:121 (same declaration text), ComparatorChallenges/BassTrace.lean:50 (same declaration text).

5. instance OAI.BassTrace.K0.relations_normal line 42

   Also declared: ComparatorChallenges/BassTorsionFree.lean:124 (same declaration text), ComparatorChallenges/BassTrace.lean:53 (same declaration text).

6. abbrev OAI.BassTrace.K0.Group line 44

   Distinct definitions of this name: ComparatorChallenges/BassTorsionFree.lean:126 (same statement text; different proof or body), ComparatorChallenges/BassTrace.lean:55 (same declaration text). Qualify references as OAI.BassTrace.K0.Group@path.

7. def OAI.BassTrace.K0.classOf line 46

   Also declared: ComparatorChallenges/BassTrace.lean:57 (same declaration text).

8. instance OAI.BassTrace.K0.groupRingRelations_normal line 50

   Also declared: ComparatorChallenges/BassTorsionFree.lean:130 (same declaration text), ComparatorChallenges/BassTrace.lean:61 (same declaration text).

9. def OAI.BassTrace.K0.rawCoefficient line 52

   Also declared: ComparatorChallenges/BassTorsionFree.lean:132 (same declaration text), ComparatorChallenges/BassTrace.lean:63 (same declaration text).

10. def OAI.BassTrace.K0.classTrace line 59

    Also declared: ComparatorChallenges/BassTrace.lean:70 (same declaration text).

11. def OAI.BassTrace.K0.rawTrace line 62

    Distinct definitions of this name: ComparatorChallenges/BassTrace.lean:73 (same statement text; different proof or body). Qualify references as OAI.BassTrace.K0.rawTrace@path.

12. def OAI.BassTrace.K0.HattoriStallings line 66

    Also declared: ComparatorChallenges/BassTrace.lean:76 (same declaration text).

13. instance OAI.BassTrace.RightProjective.rightModuleIdentityRingHomInvPair line 190

    Also declared: ComparatorChallenges/BassTrace.lean:200 (same declaration text).

14. def OAI.BassTrace.RightProjective.unopTranspose line 193

    Also declared: ComparatorChallenges/BassTrace.lean:203 (same declaration text).

15. def OAI.BassTrace.RightProjective.rightMatrix line 196

    Also declared: ComparatorChallenges/BassTrace.lean:206 (same declaration text).

16. structure OAI.BassTrace.RightProjective.Retraction line 199

    Also declared: ComparatorChallenges/BassTrace.lean:209 (same declaration text).

17. def OAI.BassTrace.RightProjective.Retraction.idempotent line 208

    Also declared: ComparatorChallenges/BassTrace.lean:218 (same declaration text).

18. def OAI.BassTrace.RightProjective.Retraction.transport line 232

    Also declared: ComparatorChallenges/BassTrace.lean:242 (same declaration text).

19. def OAI.BassTrace.RightProjective.freeSplit line 241

    Also declared: ComparatorChallenges/BassTrace.lean:251 (same declaration text).

20. def OAI.BassTrace.RightProjective.Retraction.prod line 245

    Also declared: ComparatorChallenges/BassTrace.lean:255 (same declaration text).

21. structure OAI.BassTrace.RightProjective.Object line 265

    Also declared: ComparatorChallenges/BassTrace.lean:275 (same declaration text).

22. def OAI.BassTrace.RightProjective.Object.prod line 276

    Also declared: ComparatorChallenges/BassTrace.lean:286 (same declaration text).

23. def OAI.BassTrace.RightProjective.Object.retraction line 279

    Also declared: ComparatorChallenges/BassTrace.lean:289 (same declaration text).

24. def OAI.BassTrace.RightProjective.Object.presentationClass line 284

    Also declared: ComparatorChallenges/BassTrace.lean:294 (same declaration text).

25. def OAI.BassTrace.RightProjective.moduleRelationGenerators line 287

    Also declared: ComparatorChallenges/BassTrace.lean:297 (same declaration text).

26. def OAI.BassTrace.RightProjective.moduleRelations line 293

    Also declared: ComparatorChallenges/BassTrace.lean:303 (same declaration text).

27. abbrev OAI.BassTrace.RightProjective.ModuleK0 line 296

    Also declared: ComparatorChallenges/BassTrace.lean:306 (same declaration text).

28. def OAI.BassTrace.RightProjective.rawPresentation line 299

    Also declared: ComparatorChallenges/BassTrace.lean:309 (same declaration text).

29. def OAI.BassTrace.RightProjective.presentation line 302

    Also declared: ComparatorChallenges/BassTrace.lean:312 (same declaration text).

30. def OAI.BassTrace.RightProjective.HattoriStallings line 457

    Also declared: ComparatorChallenges/BassTrace.lean:467 (same declaration text).