OAI/GroupTheory/PolycyclicRecognition/Lattices/SmoothRealActionLattice.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A cyclic lattice in a smooth real-action extension

The remaining algebraic obligation in an application is to construct the real action with the stated time-one automorphism.

  1. theorem OAI.PolycyclicRecognition.smooth_realAction_cyclic_lattice line 21