OAI/GroupTheory/PolycyclicRecognition/Analysis/ConeIdealInnerHaar.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One ideal Haar measure for both boxes and ambient conjugation

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coneIdeal_inner_invariant_haar line 29
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealInnerAutomorphism_exp_conjugation line 84