OAI/Analysis/MutuallyUnbiased/Cubic/CubicRoots.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.omega_ne_one line 10
2. theorem OAI.MUB6.omega_sq_ne_one line 12
3. theorem OAI.MUB6.omega_sq_ne_omega line 17
4. theorem OAI.MUB6.omega_re line 22
5. theorem OAI.MUB6.omega_sq_re line 28
6. theorem OAI.MUB6.cube_roots_three line 31
7. theorem OAI.MUB6.cube_root_real_indicator line 44
8. theorem OAI.MUB6.cube_roots_one_count line 54

   Source documentation

   Six cube roots summing to zero contain the root one exactly twice.

   theorem cube_roots_one_count (v : Coord → ℂ) (hv : ∀ i, v i ^ 3 = 1)
       (hs : ∑ i, v i = 0) : (Finset.univ.filter (fun i => v i = 1)).card = 2 := by
   …

   Mentions: OAI.MUB6.Coord

9. theorem OAI.MUB6.cube_roots_each_count line 70

   Source documentation

   Every cube root occurs twice among six cube roots whose sum vanishes.

   theorem cube_roots_each_count (v : Coord → ℂ) (hv : ∀ i, v i ^ 3 = 1)
       (hs : ∑ i, v i = 0) (a : ℂ) (ha : a ^ 3 = 1) :
       (Finset.univ.filter (fun i => v i = a)).card = 2 := by
   …

   Mentions: OAI.MUB6.Coord