OAI/LinearAlgebra/Hadamard/Basic.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Unit entries, orthogonality, characters and the cubic matrix.

  1. abbrev OAI.HadamardSix.Index line 11

    Also declared: ComparatorChallenges/HadamardCubeFiber.lean:11 (same declaration text).

  2. abbrev OAI.HadamardSix.Matrix6 line 12

    Also declared: ComparatorChallenges/HadamardCubeFiber.lean:12 (same declaration text).

  3. abbrev OAI.HadamardSix.Charge line 13
  4. def OAI.HadamardSix.Unimodular line 15

    Also declared: ComparatorChallenges/HadamardCubeFiber.lean:14 (same declaration text).

  5. def OAI.HadamardSix.IsComplexHadamard line 17

    Also declared: ComparatorChallenges/HadamardCubeFiber.lean:16 (same declaration text).

  6. def OAI.HadamardSix.HadamardEquivalent line 20
  7. def OAI.HadamardSix.Balanced line 25
  8. def OAI.HadamardSix.character line 27
  9. def OAI.HadamardSix.g line 30
  10. def OAI.HadamardSix.permuteCharge line 33
  11. def OAI.HadamardSix.alpha line 35
  12. def OAI.HadamardSix.omega line 37
  13. def OAI.HadamardSix.taoExponent line 39
  14. def OAI.HadamardSix.taoMatrix line 45
  15. lemma OAI.HadamardSix.unit_ne_zero line 47
  16. lemma OAI.HadamardSix.unit_mul_star line 51
  17. lemma OAI.HadamardSix.unit_star_mul line 55
  18. lemma OAI.HadamardSix.unit_inv line 59
  19. lemma OAI.HadamardSix.Unimodular.entry_ne_zero line 63
  20. lemma OAI.HadamardSix.IsComplexHadamard.unimodular line 66
  21. lemma OAI.HadamardSix.IsComplexHadamard.mul_conjTranspose line 69
  22. lemma OAI.HadamardSix.IsComplexHadamard.column_orthogonality line 79
  23. lemma OAI.HadamardSix.IsComplexHadamard.row_orthogonality line 85
  24. lemma OAI.HadamardSix.isComplexHadamard_of_rows line 91
  25. lemma OAI.HadamardSix.IsComplexHadamard.transpose line 106
  26. lemma OAI.HadamardSix.IsComplexHadamard.conjugate line 112