OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialExteriorShiftOperators.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.polynomialExteriorMul line 14
2. theorem OAI.PolycyclicRecognition.polynomialExteriorMul_commute line 17
3. def OAI.PolycyclicRecognition.polynomialExteriorShiftEvaluation line 28
4. theorem OAI.PolycyclicRecognition.polynomialExteriorShiftEvaluation_X line 33
5. theorem OAI.PolycyclicRecognition.polynomialExteriorMul_scalarDifference line 38
6. theorem OAI.PolycyclicRecognition.polynomialExterior_relation_detected line 52

   Source documentation

   A relation among operators restricting to polynomial exterior shifts is also a relation among the corresponding products in independent variables.

   theorem polynomialExterior_relation_detected {W : Type} [AddCommGroup W] [Module K W]
       (n k : ℕ) (c : Fin k → K)
       (α : MvPolynomial (Fin k) K →ₐ[K] Module.End K W)
       (E : (⋀[K]^n K[X]) →ₗ[K] W) (hE : Function.Injective E)
       (hα : ∀ i w, E (polynomialExteriorMul K n (Polynomial.C (c i) - Polynomial.X) w) =
         α (MvPolynomial.X i) (E w))
       {p : MvPolynomial (Fin k) K} (hp : α p = 0) :
       MvPolynomial.aeval (fun i => shiftProduct K n (c i)) p = 0 := by
   …

   Mentions: OAI.PolycyclicRecognition.polynomialExteriorMul, OAI.PolycyclicRecognition.shiftProduct