OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialLangTransversal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Lang transversals from an invertible leading term

All nonlinear errors raise the finite lower central filtration. The inverse is therefore obtained by the finite correction algorithm already constructed.

  1. theorem OAI.PolycyclicRecognition.polynomial_transversal_bijective line 18