OAI/GroupTheory/UniversalGroup/Idempotents.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.UniversalFInfinity.IdempotentSystems.algebraRing line 22
2. def OAI.UniversalFInfinity.IdempotentSystems.corner line 25
3. def OAI.UniversalFInfinity.IdempotentSystems.carrier line 29
4. lemma OAI.UniversalFInfinity.IdempotentSystems.carrier_finite line 32
5. lemma OAI.UniversalFInfinity.IdempotentSystems.one_mem line 40
6. lemma OAI.UniversalFInfinity.IdempotentSystems.corner_mem line 42
7. lemma OAI.UniversalFInfinity.IdempotentSystems.carrier_idempotent line 46
8. lemma OAI.UniversalFInfinity.IdempotentSystems.sum_idempotent line 52
9. lemma OAI.UniversalFInfinity.IdempotentSystems.diagonalUnit_eq_diagonal line 59
10. lemma OAI.UniversalFInfinity.IdempotentSystems.corner_diagonal line 68
11. lemma OAI.UniversalFInfinity.IdempotentSystems.projection_mem line 75
12. lemma OAI.UniversalFInfinity.IdempotentSystems.projection_first_sum line 79
13. lemma OAI.UniversalFInfinity.IdempotentSystems.projection_mul_zero line 88
14. lemma OAI.UniversalFInfinity.IdempotentSystems.projection_orthogonal line 93
15. def OAI.UniversalFInfinity.IdempotentSystems.AdditiveOnDiagram line 99
16. lemma OAI.UniversalFInfinity.IdempotentSystems.restrict_additive line 103
17. lemma OAI.UniversalFInfinity.IdempotentSystems.projection_multiples line 114
18. lemma OAI.UniversalFInfinity.IdempotentSystems.first_projection_zero line 121
19. lemma OAI.UniversalFInfinity.IdempotentSystems.first_two_mem line 148
20. lemma OAI.UniversalFInfinity.IdempotentSystems.identity_additive_decomposition line 157
21. theorem OAI.UniversalFInfinity.IdempotentSystems.annihilates_identity line 181
22. theorem OAI.UniversalFInfinity.IdempotentSystems.annihilates_identity_subtype line 188
23. def OAI.UniversalFInfinity.ConcreteEnvelopes.system line 207
24. abbrev OAI.UniversalFInfinity.ConcreteEnvelopes.P₂ line 214
25. abbrev OAI.UniversalFInfinity.ConcreteEnvelopes.P₃ line 215
26. abbrev OAI.UniversalFInfinity.ConcreteEnvelopes.Index line 216
27. abbrev OAI.UniversalFInfinity.ConcreteEnvelopes.triples line 217
28. structure OAI.UniversalFInfinity.ConcreteEnvelopes.IsDiagram line 219
29. theorem OAI.UniversalFInfinity.ConcreteEnvelopes.finite_envelope line 224
30. def OAI.UniversalFInfinity.ConcreteEnvelopes.IsUniversal line 232
31. theorem OAI.UniversalFInfinity.ConcreteEnvelopes.self_maps line 236
32. theorem OAI.UniversalFInfinity.ConcreteEnvelopes.coprime_annihilation line 251