OAI/GroupTheory/PolycyclicRecognition/Algebra/EigenlinePingPong.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ping-pong from transverse eigenline cones

The source-cone constants are constructed from the actual functionals and vectors. Only the spectral gaps, transversality and disjointness of the specified cones remain as geometric data.

  1. theorem OAI.PolycyclicRecognition.free_powers_of_transverse_eigenline_cones line 19