OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanLinkedProbePaths.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 line 28

    Source comment

    The original sampling center is retained throughout all three paths.
    theorem exists_linked_probe_paths
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput