OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentPowerSeriesEvaluation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite evaluation of rational power series at a nilpotent element

Evaluation takes place in the given associative algebra, which need not be commutative. Nilpotence makes truncation invisible to polynomial evaluation.

  1. theorem OAI.PolycyclicRecognition.powerSeries_trunc_monomial line 16
  2. theorem OAI.PolycyclicRecognition.aeval_powerSeries_trunc_coe line 35
  3. def OAI.PolycyclicRecognition.nilpotentPowerSeriesEval line 48
  4. theorem OAI.PolycyclicRecognition.nilpotentPowerSeriesEval_coe line 57