OAI/RingTheory/DirectFiniteness/GluedWords.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.KaplanskyCounterexample.GluedGroup.totalMapline 13 - lemma
OAI.KaplanskyCounterexample.GluedGroup.totalMap_of_memline 16 - def
OAI.KaplanskyCounterexample.GluedGroup.signedTokenline 19 - def
OAI.KaplanskyCounterexample.GluedGroup.Allowedline 22 - lemma
OAI.KaplanskyCounterexample.GluedGroup.signedToken_invline 26 - lemma
OAI.KaplanskyCounterexample.GluedGroup.allowed_invline 31 - lemma
OAI.KaplanskyCounterexample.GluedGroup.allowed_cancelline 60