OAI/Analysis/MutuallyUnbiased/Cubic/CubicClassification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.hadamard_square_equivalent_tao line 13

   Source documentation

   The cubic classification from the companion: no restriction is imposed on the complex entries or on the unit phases in the equivalence relation.

   theorem hadamard_square_equivalent_tao {H : CMatrix} (hH : IsHadamard H)
       (hH2 : IsHadamard (fun i j => H i j ^ 2)) : Equivalent H tao := by
   …

   Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Equivalent, OAI.MUB6.tao