OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialMatrixFunctions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Polynomial matrix exponentials and logarithms with uniform truncation

  1. theorem OAI.PolycyclicRecognition.multivariatePolynomialFunctions_const line 13
  2. theorem OAI.PolycyclicRecognition.multivariatePolynomialFunctions_mul line 17
  3. def OAI.PolycyclicRecognition.HasPolynomialMatrixEntries line 26
  4. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.linear line 34
  5. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.linear_image line 44
  6. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.const line 62
  7. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.add line 66
  8. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.sub line 70
  9. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.smul line 74
  10. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.mul line 78
  11. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.pow line 87
  12. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.sum line 93
  13. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.exp_of_pow_eq_zero line 104
  14. theorem OAI.PolycyclicRecognition.HasPolynomialMatrixEntries.finiteLog line 119