OAI/GroupTheory/PolycyclicRecognition/Lattices/PolynomialLatticeExtension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial maps of lattices extend as group maps

Multiplication identities on integral coordinates determine the identity on all real coordinates. Polynomial inverse identities extend in the same way.

  1. theorem OAI.PolycyclicRecognition.coordinatePolynomial_mul_of_integer_mul line 24
  2. def OAI.PolycyclicRecognition.coordinatePolynomialHomFromIntegerGrid line 47
  3. theorem OAI.PolycyclicRecognition.coordinatePolynomial_leftInverse_of_integer line 65
  4. def OAI.PolycyclicRecognition.coordinatePolynomialEquivFromIntegerGrid line 75