OAI/Combinatorics/Progressions/Polynomial/LieCoordinatePolynomials.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.lieStructureConstants line 15
2. theorem OAI.Erdos3.lie_coordinate_formula line 18
3. def OAI.Erdos3.coordinateRightBracket line 33
4. def OAI.Erdos3.coordinateBracketList line 37
5. def OAI.Erdos3.dynkinCoordinatePolynomial line 42
6. theorem OAI.Erdos3.coordinateRightBracket_eval line 46
7. theorem OAI.Erdos3.coordinateBracketList_eval line 56
8. theorem OAI.Erdos3.dynkinCoordinatePolynomial_eval line 69
9. theorem OAI.Erdos3.coordinateRightBracket_totalDegree line 78
10. theorem OAI.Erdos3.coordinateBracketList_totalDegree line 90
11. theorem OAI.Erdos3.dynkinCoordinatePolynomial_totalDegree line 101
12. def OAI.Erdos3.bchCoordinatePolynomial line 109
13. theorem OAI.Erdos3.bchCoordinatePolynomial_eval line 114
14. theorem OAI.Erdos3.bchCoordinatePolynomial_totalDegree line 124