OAI/Algebra/OddKaplansky/Cellular.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.Cellular.rightShift line 12
2. def OAI.OddKaplansky.Cellular.shift line 16
3. def OAI.OddKaplansky.Cellular.operator line 20
4. lemma OAI.OddKaplansky.Cellular.operator_single line 21
5. lemma OAI.OddKaplansky.Cellular.operator_formula line 24
6. lemma OAI.OddKaplansky.Cellular.operator_mul line 27
7. lemma OAI.OddKaplansky.Cellular.operator_one line 28
8. lemma OAI.OddKaplansky.Cellular.indicator_eval line 29
9. lemma OAI.OddKaplansky.Cellular.operator_injective line 36
10. def OAI.OddKaplansky.Cellular.IsCellular line 41
11. lemma OAI.OddKaplansky.Cellular.operator_cellular line 43
12. lemma OAI.OddKaplansky.Cellular.left_inverse line 48
13. lemma OAI.OddKaplansky.Cellular.range_eq line 51
14. lemma OAI.OddKaplansky.Cellular.missing_indicator line 59
15. lemma OAI.OddKaplansky.Cellular.theorem_all_configurations line 68