OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanMappedTemplatePaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual image paths from the selected affine profiles

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_mapped_template_profile_paths line 27

    Source documentation

    Good profiles on all selected prefixes give paths in the actual target space, centered at the image of the starting point. Their height region is the affine image of the translated template, with the offset cancelled.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput