OAI/NumberTheory/Ostmann/Characters/BinaryHaar.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.BinaryHaar.Leaves line 9
  2. def OAI.Ostmann.Characters.BinaryHaar.Splits line 13
  3. instance OAI.Ostmann.Characters.BinaryHaar.leavesFintype line 17
  4. instance OAI.Ostmann.Characters.BinaryHaar.splitsFintype line 22
  5. def OAI.Ostmann.Characters.BinaryHaar.decoratedSplit line 27
  6. def OAI.Ostmann.Characters.BinaryHaar.expose line 34
  7. def OAI.Ostmann.Characters.BinaryHaar.product line 42
  8. theorem OAI.Ostmann.Characters.BinaryHaar.expose_first line 46
  9. def OAI.Ostmann.Characters.BinaryHaar.fixedProductEquiv line 52
  10. theorem OAI.Ostmann.Characters.BinaryHaar.expose_average line 66
  11. theorem OAI.Ostmann.Characters.BinaryHaar.fixedProduct_card line 72