Complex 3rd root of unity

Stream: new members

[Maris Ozols]

I'm trying to show something very basic: if ω = exp (2 * π * I / 3) then ω ≠ 1. I get stuck at ↑n * 3 = 1 which should give me a contradiction since n is an integer. Does anyone know how to get rid of n being coerced from an integer to a complex number? Also, if anyone knows a shorter proof of this, I would be very happy to see it.

import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Log

open Complex Real

noncomputable def ω : ℂ := exp (2 * π * I / 3)

lemma omega_ne_one : ω ≠ 1 := by
  intro h
  unfold ω at h
  rw [Complex.exp_eq_one_iff] at h
  obtain ⟨n, h⟩ := h
  rw [div_eq_iff (by norm_num)] at h
  nth_rw 4 [mul_comm] at h
  nth_rw 2 [mul_assoc] at h
  have ne_zero : 2 * ↑π * I ≠ 0 := by
    norm_num
    exact pi_ne_zero
  rw [left_eq_mul₀ ne_zero] at h
  clear ne_zero
  have : 3 ∣ 1 := by
    sorry
  simp only [Nat.dvd_one, OfNat.ofNat_ne_one] at this

[Ruben Van de Velde]

Does norm_cast at this work?

[Riccardo Brasca]

You can do something like

import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Log

open Complex Real

noncomputable def ω : ℂ := exp (2 * π * I / 3)

lemma omega_ne_one : ω ≠ 1 := by
  intro h
  unfold ω at h
  rw [Complex.exp_eq_one_iff] at h
  obtain ⟨n, h⟩ := h
  rw [div_eq_iff (by norm_num)] at h
  nth_rw 4 [mul_comm] at h
  nth_rw 2 [mul_assoc] at h
  have ne_zero : 2 * ↑π * I ≠ 0 := by
    norm_num
    exact pi_ne_zero
  rw [left_eq_mul₀ ne_zero] at h
  replace h : (n : ℂ) * ((3 : ℤ) : ℂ) = ((1 : ℤ) : ℂ) := by  simpa
  norm_cast at h
  have : ¬((3 : ℤ) ∣ 1) := by norm_num
  apply this
  use n
  grind

[Riccardo Brasca]

replacing simpa with simpa? will tell you the lemma you need (in the other direction), if you want to avoid the replace h part.

[Riccardo Brasca]

ah, norm_cast is smart enough to avoid the replace part, even better

[Maris Ozols]

Thanks, that worked! I wasn't aware of the norm_cast tactic.

[Kenny Lau]

import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Log

open Complex Real

noncomputable def ω : ℂ := exp (2 * π * I / 3)

lemma omega_ne_one : ω ≠ 1 := by
  suffices re ω = - 1/2 from
    fun h ↦ absurd this <| h ▸ by norm_num
  calc
    ω.re = Real.cos (2 * π / 3) := by simp [ω, Complex.exp_re]
       _ = -1/2 := by rw [mul_div_assoc, Real.cos_two_mul]; norm_num

[Ruben Van de Velde]

Maybe

import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Log

open Complex Real

noncomputable def ω : ℂ := exp (2 * π * I / 3)

lemma omega_ne_one : ω ≠ 1 := by
  suffices re ω = - 1/2 from
    fun h => by norm_num [h] at this
  calc
    ω.re = Real.cos (2 * π / 3) := by simp [ω, Complex.exp_re]
       _ = -1/2 := by rw [mul_div_assoc, Real.cos_two_mul]; norm_num

[Maris Ozols]

Thanks a lot! Will have to digest this.