complex inequality

Stream: new members

[东禹]

noncomputable def ω : ℂ := Complex.exp (2 * Real.pi * I / 3)

lemma ω_prop : ω ^ 3 = 1 ∧ ω ≠ 1 := by
  constructor
  · simp [ω, div_eq_mul_inv,← Complex.exp_nat_mul]
    rw [mul_comm]
    rw [ mul_assoc ]
    simp
  · sorry

How do I complete this proof?TT

[Notification Bot]

This topic was moved here from #lean4 > complex inequality by Kevin Buzzard.

[Yiming Fu]

import Mathlib

open Complex

noncomputable def ω : ℂ := Complex.exp (2 * Real.pi * I / 3)

lemma ω_prop : ω ^ 3 = 1 ∧ ω ≠ 1 := by
  constructor
  · simp [ω, div_eq_mul_inv,← Complex.exp_nat_mul]
    rw [mul_comm]
    rw [ mul_assoc ]
    simp
  · simp only [ω, ne_eq, Complex.ext_iff, one_re, one_im]
    rintro ⟨_, him⟩
    rw [Complex.exp_im] at him
    simp at him
    have : Real.sin (2 * Real.pi / 3) = √3 / 2 :=
      calc
        _ = Real.sin (Real.pi - Real.pi / 3) := by ring_nf
        _ = _ := by simp
    rw [this] at him
    norm_num at him

[东禹]

Thank you！