OAI/Algebra/OddKaplansky/IdempotentFree.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OddKaplansky.IdempotentFree.range_fixed line 17
2. lemma OAI.OddKaplansky.IdempotentFree.split line 21
3. lemma OAI.OddKaplansky.IdempotentFree.projective line 28
4. lemma OAI.OddKaplansky.IdempotentFree.free line 31
5. def OAI.OddKaplansky.IdempotentFree.J line 38
6. def OAI.OddKaplansky.IdempotentFree.Y line 40
7. lemma OAI.OddKaplansky.IdempotentFree.single_sum line 43
8. lemma OAI.OddKaplansky.IdempotentFree.YJ line 47
9. lemma OAI.OddKaplansky.IdempotentFree.JY line 73
10. lemma OAI.OddKaplansky.IdempotentFree.rectangular line 101