OAI/GroupTheory/PolycyclicRecognition/Geometry/RationalRootSurjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rational surjectivity from positive powers in the image

  1. theorem OAI.PolycyclicRecognition.rational_map_surjective_of_roots line 13
  2. theorem OAI.PolycyclicRecognition.abelian_finite_rational_rank_of_rootCore line 39