OAI/GroupTheory/PolycyclicRecognition/Geometry/FiniteExponentialLogarithm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite exponential and logarithm identities

Formal power-series identities evaluate in an associative rational algebra at a nilpotent element. All expressions are finite polynomials.

  1. def OAI.PolycyclicRecognition.finiteNilpotentLog line 18
  2. theorem OAI.PolycyclicRecognition.nilpotentPowerSeriesEval_exp line 21
  3. theorem OAI.PolycyclicRecognition.finiteNilpotentLog_pow line 30
  4. theorem OAI.PolycyclicRecognition.finiteNilpotentLog_exp line 34
  5. theorem OAI.PolycyclicRecognition.exp_finiteNilpotentLog line 43