OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialExteriorDeterminant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coordinates on the exterior power of a free polynomial orbit

Evaluation at independent variables followed by the determinant sends a polynomial wedge to its alternant. Multiplication by a shifted variable in every coordinate becomes multiplication by the corresponding product.

  1. def OAI.PolycyclicRecognition.polynomialEvaluationVector line 19
  2. def OAI.PolycyclicRecognition.scalarDeterminantAlternating line 23
  3. def OAI.PolycyclicRecognition.polynomialDeterminantAlternating line 30
  4. def OAI.PolycyclicRecognition.polynomialExteriorDeterminant line 34
  5. theorem OAI.PolycyclicRecognition.polynomialExteriorDeterminant_value line 38
  6. theorem OAI.PolycyclicRecognition.polynomialExteriorDeterminant_mul line 43
  7. theorem OAI.PolycyclicRecognition.polynomialExteriorDeterminant_shift line 61
  8. theorem OAI.PolycyclicRecognition.polynomialExteriorDeterminant_monomials line 74
  9. theorem OAI.PolycyclicRecognition.polynomialExteriorDeterminant_monomials_ne_zero line 86