OAI/Combinatorics/Progressions/Geometry/LieStructureTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.transportedLieConstants line 15
2. theorem OAI.Erdos3.transportedLieConstants_height line 20
3. theorem OAI.Erdos3.transportedLieConstants_formula line 36
4. theorem OAI.Erdos3.basisMatrix_mulVec line 54
5. theorem OAI.Erdos3.basisMatrix_injective line 61
6. theorem OAI.Erdos3.basisMatrix_surjective line 68
7. theorem OAI.Erdos3.lieStructureConstants_embedding line 77
8. theorem OAI.Erdos3.lieStructureConstants_section line 93
9. theorem OAI.Erdos3.basisMatrix_section line 107
10. theorem OAI.Erdos3.lieStructureConstants_quotient_matrix line 116