OAI/Combinatorics/Progressions/Geometry/LieCoordinateScalarExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.lie_coordinate_formula_over line 14
2. theorem OAI.Erdos3.coordinateRightBracket_eval_over line 31
3. theorem OAI.Erdos3.coordinateBracketList_eval_over line 43
4. theorem OAI.Erdos3.dynkinCoordinatePolynomial_eval_over line 56
5. theorem OAI.Erdos3.bchCoordinatePolynomial_eval_over line 67
6. theorem OAI.Erdos3.exists_bch_coordinate_polynomials_over_exp_height line 78