OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanHeightPublishedAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing all nilpotent models in the uniform Cartan height theorem

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_height_of_published_inputs line 32

    Source documentation

    Factor models, cone models, charts and measures are selected internally from the cited nilpotent existence, integration, Haar and Dynkin inputs.

    theorem exists_uniform_height_of_published_inputs
    (nilp : NilpotentPublishedInputs)
    (integrateN : ∀ N : NilpotentLieModel (cartanRootIdeal H),
      NilpotentLieIntegrationInput (EN := N.modelSpace) (N := N.carrier) (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.NilpotentPublishedInputs, OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.NilpotentLieIntegrationInput