OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteCyclicOrbit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A dependent invertible cyclic orbit spans a finite-dimensional space

  1. theorem OAI.PolycyclicRecognition.finite_cyclic_invariant_all line 15
  2. theorem OAI.PolycyclicRecognition.cyclic_orbit_span_finite_of_dependent line 47
  3. theorem OAI.PolycyclicRecognition.cyclic_orbit_span_finite_of_finite_exterior line 121