def
definition
rootOfUnity
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.ImaginaryUnit on GitHub at line 191.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
188
189 These are exactly the 8-tick phases!
190 They form a group under multiplication (cyclic group Z₈). -/
191noncomputable def rootOfUnity (k : Fin 8) : ℂ :=
192 cexp (I * (2 * Real.pi * k / 8))
193
194/-- The roots form a group. -/
195theorem roots_form_group :
196 ∀ j k : Fin 8, rootOfUnity j * rootOfUnity k = rootOfUnity (j + k) := by
197 intro j k
198 unfold rootOfUnity
199 rw [← Complex.exp_add]
200 push_cast
201 have h_val : ((j + k : Fin 8).val : ℝ) = ((j.val + k.val) % 8 : ℕ) := by
202 simp only [Fin.val_add]
203 rw [h_val]
204 have h_div : (j.val + k.val : ℕ) = ((j.val + k.val) % 8) + 8 * ((j.val + k.val) / 8) := by
205 rw [add_comm, Nat.div_add_mod]
206 push_cast
207 rw [h_div]
208 rw [mul_add, add_div, mul_add]
209 rw [← Complex.exp_add]
210 congr 1
211 · ring
212 · have h_period : I * (2 * Real.pi * (8 * ((j.val + k.val) / 8)) / 8) = I * (2 * Real.pi * ((j.val + k.val) / 8)) := by
213 ring
214 rw [h_period]
215 rw [mul_comm I, ← mul_assoc]
216 rw [Complex.exp_int_mul_two_pi_mul_I ((j.val + k.val) / 8)]
217 simp
218
219/-! ## Falsification Criteria -/
220
221/-- The derivation would be falsified if: