OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSegmentCellPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From recurrent good sheets to the actual Cartan support inequality

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.templateSupport_le_of_recurrent_segment_cells_sequence line 41

    Source documentation

    Whole good segment legs, the actual pivot visits and recurrent sheet volume imply the support inequality. No separate path or switch estimate is assumed.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput