OAI/Analysis/MutuallyUnbiased/Model.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MUB6.Coord line 10

   Also declared: ComparatorChallenges/MUBSix.lean:10 (same declaration text).

2. abbrev OAI.MUB6.CMatrix line 11

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

3. abbrev OAI.MUB6.Charge line 12

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

4. def OAI.MUB6.IsHadamard line 14

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

5. def OAI.MUB6.character line 18

   Also declared: ComparatorChallenges/MUBSix.lean:18 (same declaration text).

6. def OAI.MUB6.g line 20

   Also declared: ComparatorChallenges/MUBSix.lean:20 (same declaration text).

7. def OAI.MUB6.alpha line 23

   Also declared: ComparatorChallenges/MUBSix.lean:23 (same declaration text).

8. def OAI.MUB6.permuteCharge line 25

   Also declared: ComparatorChallenges/MUBSix.lean:25 (same declaration text).

9. def OAI.MUB6.Equivalent line 28

   Source documentation

   Full Hadamard equivalence, with arbitrary unit complex phases.

   Also declared: ComparatorChallenges/MUBSix.lean:28 (same declaration text).

   def Equivalent (H K : CMatrix) : Prop :=
   …

   Mentions: OAI.MUB6.CMatrix

10. def OAI.MUB6.omega line 33

    Also declared: ComparatorChallenges/MUBSix.lean:33 (same declaration text).

11. def OAI.MUB6.taoExponent line 37

    Source documentation

    The five-cycle exponent matrix in equation (cubic-matrix). The entries 2 represent the exponents -1 modulo three.

    Also declared: ComparatorChallenges/MUBSix.lean:37 (same declaration text).

    def taoExponent : Matrix Coord Coord ℕ :=
    …

    Mentions: OAI.MUB6.Coord

12. def OAI.MUB6.tao line 45

    Also declared: ComparatorChallenges/MUBSix.lean:45 (same declaration text).

13. abbrev OAI.MUB6.Space line 47

    Also declared: ComparatorChallenges/MUBSix.lean:47 (same declaration text).

14. abbrev OAI.MUB6.Basis line 48

    Also declared: ComparatorChallenges/MUBSix.lean:48 (same declaration text).

15. def OAI.MUB6.IsMUBFamily line 50

    Also declared: ComparatorChallenges/MUBSix.lean:50 (same declaration text).

16. def OAI.MUB6.Attainable line 54

    Also declared: ComparatorChallenges/MUBSix.lean:54 (same declaration text).