OAI/Combinatorics/Progressions/Geometry/CoordinateDeterminant.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.coordinateMatrixPolynomial line 11
2. theorem OAI.Erdos3.coordinateMatrixPolynomial_eval line 14
3. theorem OAI.Erdos3.coordinateMatrixPolynomial_degree line 24
4. def OAI.Erdos3.coordinateDeterminantVariation line 32
5. theorem OAI.Erdos3.coordinateDeterminantVariation_nonneg line 35
6. theorem OAI.Erdos3.coordinateMatrixPolynomial_derivative line 40
7. theorem OAI.Erdos3.coordinateMatrixPolynomial_variation line 54