OAI/LinearAlgebra/Hadamard/Main.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The dichotomy implied by the two Fourier product identities.

  1. def OAI.HadamardSix.crossCharge line 11
  2. def OAI.HadamardSix.sameCharge line 13
  3. lemma OAI.HadamardSix.crossCharge_eq line 15
  4. lemma OAI.HadamardSix.sameCharge_eq line 16
  5. def OAI.HadamardSix.pairOrdering line 18
  6. lemma OAI.HadamardSix.pairOrdering_bijective line 56
  7. lemma OAI.HadamardSix.double_difference_transport line 60
  8. lemma OAI.HadamardSix.dichotomy_of_product_identities line 71