OAI/Algebra/Finitistic/Selection/SelectionAlgebra.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectionRing line 13
2. def OAI.LittleFinitistic.algebraZ line 15
3. theorem OAI.LittleFinitistic.algebraZ_square line 17
4. theorem OAI.LittleFinitistic.algebraZ_central line 21
5. def OAI.LittleFinitistic.selectionIdempotent line 24
6. theorem OAI.LittleFinitistic.selectionIdempotent_square line 27
7. theorem OAI.LittleFinitistic.selectionIdempotent_central line 36
8. def OAI.LittleFinitistic.selectionAutomorphism line 44
9. theorem OAI.LittleFinitistic.selectionAutomorphism_z line 47
10. theorem OAI.LittleFinitistic.selectionAutomorphism_idempotent line 51