OAI/GroupTheory/PolycyclicRecognition/Algebra/CoordinatePolynomial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial restrictions to coordinate lines

  1. def OAI.PolycyclicRecognition.CoordinatePolynomial line 15

    Source documentation

    Each coordinate-line restriction is a polynomial of degree at most D.

    def CoordinatePolynomial (n D : ℕ) (f : (Fin n → ℝ) → ℝ) : Prop :=
…
  2. theorem OAI.PolycyclicRecognition.CoordinatePolynomial.head line 19
  3. theorem OAI.PolycyclicRecognition.CoordinatePolynomial.tail line 25
  4. theorem OAI.PolycyclicRecognition.coordinatePolynomial_eval line 32