OAI/NumberTheory/Ostmann/Arithmetic/TreePermutationHaar.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.TreePermutationHaar.leafIndex line 11
  2. abbrev OAI.Ostmann.Arithmetic.TreePermutationHaar.blocks line 16
  3. def OAI.Ostmann.Arithmetic.TreePermutationHaar.componentIndex line 19
  4. def OAI.Ostmann.Arithmetic.TreePermutationHaar.leftPartition line 22
  5. theorem OAI.Ostmann.Arithmetic.TreePermutationHaar.rightComponent_surjective line 28
  6. def OAI.Ostmann.Arithmetic.TreePermutationHaar.rightPartition line 37
  7. def OAI.Ostmann.Arithmetic.TreePermutationHaar.leafPairEquiv line 45
  8. theorem OAI.Ostmann.Arithmetic.TreePermutationHaar.fiberProduct_equiv line 52
  9. theorem OAI.Ostmann.Arithmetic.TreePermutationHaar.left_componentProduct line 59
  10. theorem OAI.Ostmann.Arithmetic.TreePermutationHaar.right_componentProduct line 69
  11. theorem OAI.Ostmann.Arithmetic.TreePermutationHaar.coupled_iff line 79
  12. def OAI.Ostmann.Arithmetic.TreePermutationHaar.coupledEquiv line 90
  13. instance OAI.Ostmann.Arithmetic.TreePermutationHaar.coupledTreeFintype line 96
  14. theorem OAI.Ostmann.Arithmetic.TreePermutationHaar.tree_products_uniform line 100