OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialGrowthImages.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The concrete polynomial-growth matrix image has no free pair

  1. theorem OAI.PolycyclicRecognition.polynomial_growth_surjective_image line 11
  2. theorem OAI.PolycyclicRecognition.polynomial_growth_image_no_free_pair line 25
  3. theorem OAI.PolycyclicRecognition.polynomial_growth_linear_image_no_free_pair line 41