OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPivotProbePaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Image paths from the actual linked profile bounds

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_linked_probe_paths_with_pivot line 30

    Source documentation

    The compact profile restriction can also contain the contact pivot. This gives the base and terminal profile bounds on the same set used by every path.

    theorem exists_linked_probe_paths_with_pivot
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput