OAI/Analysis/Cotype/WalshSymmetry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.walshSymmetryGroup line 10
  2. abbrev OAI.Cotype.WalshSymmetry line 22
  3. instance OAI.Cotype.(instance at line 23) line 23
  4. instance OAI.Cotype.(instance at line 24) line 24
  5. def OAI.Cotype.primalSymmetry line 26
  6. def OAI.Cotype.dualSymmetry line 27
  7. theorem OAI.Cotype.symmetry_pairing line 29
  8. theorem OAI.Cotype.character_separates line 32
  9. theorem OAI.Cotype.primalSymmetry_xor line 39
  10. theorem OAI.Cotype.dualSymmetry_xor line 46
  11. def OAI.Cotype.l2Reindex line 58
  12. theorem OAI.Cotype.l2Reindex_apply line 70
  13. def OAI.Cotype.rightTranslation line 75
  14. theorem OAI.Cotype.rightTranslation_apply line 80