OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalPowerSeriesHom.lean
4 declarations, 0 contain sorry, 0 declared as axioms
Rational power-series homomorphisms killed by a power of the variable
- theorem
OAI.PolycyclicRecognition.rationalPowerSeriesHom_Cline 12 - theorem
OAI.PolycyclicRecognition.rationalPowerSeriesHom_polynomialline 16 - theorem
OAI.PolycyclicRecognition.rationalPowerSeriesHom_eq_truncline 26 - theorem
OAI.PolycyclicRecognition.rationalPowerSeriesHom_eq_aeval_truncline 40