OAI/GroupTheory/PolycyclicRecognition/Algebra/TransverseEigenlineFreePair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A free pair from transverse dominant eigenlines

Small disjoint cones and their source bounds are constructed from the finite family of eigenvectors and functionals. No ping-pong-domain existence hypothesis is used.

  1. theorem OAI.PolycyclicRecognition.free_powers_of_transverse_dominant_eigenlines line 19