OAI/GroupTheory/PolycyclicRecognition/Algebra/ConstructedNilpotentPublishedInputs.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Discharging the nilpotent published-input family

The finite BCH formula holds for every nilpotent Lie model. Together with the model construction, global chart, integration, and Haar identities, this proves the nilpotent input record without additional hypotheses.

  1. theorem OAI.PolycyclicRecognition.nilpotentPublishedInputs line 17

    Source documentation

    The nilpotent BCH expansion holds without additional hypotheses.

    theorem nilpotentPublishedInputs : NilpotentPublishedInputs where
…

    Mentions: OAI.PolycyclicRecognition.NilpotentPublishedInputs