OAI/GroupTheory/PolycyclicRecognition/Analysis/AscendingBaseTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transport of finite ascending bases along equivariant homomorphisms

  1. def OAI.PolycyclicRecognition.HasFinitelyGeneratedAscendingBase line 12
  2. theorem OAI.PolycyclicRecognition.automorphism_pow_equivariant line 16
  3. theorem OAI.PolycyclicRecognition.HasFinitelyGeneratedAscendingBase.of_surjective line 23
  4. theorem OAI.PolycyclicRecognition.HasFinitelyGeneratedAscendingBase.of_equiv line 38
  5. theorem OAI.PolycyclicRecognition.abelianization_map_surjective line 48

    Distinct definitions of this name: OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentFiniteRankRootCore.lean:19 (different declaration text). Qualify references as OAI.PolycyclicRecognition.abelianization_map_surjective@path.

  6. theorem OAI.PolycyclicRecognition.ascendingBase_abelianization_of_surjective line 55