fin N subtraction of non equal nums cannot give zero

Stream: new members

[MohanadAhmed]

I am trying to prove that if I have two non -equal fin N numbers then the result cannot zero. I am stuck. Any thoughts or help appreciated.

example {N : ℕ}
  {hN : 1 < N}
  (k n : fin N)
  (h : ¬k = n)
  (hkn : (↑k:ℤ) - ↑n = 0) :
  false :=
begin
  sorry,
end

This is part of proving that a complex exponential exp(2*pi*I*(k - n)/N) is not one unless k and n are the same.

example {N : ℕ}
  {hN : 1 < N}
  (k n : fin N)
  (h : ¬k = n)
  (hc : exp (2 * ↑π * I * (↑k - ↑n) / ↑N) = 1) :
  false :=
begin
  rw complex.exp_eq_one_iff at hc,
  cases hc with M hM,
sorry,
end

[Ruben Van de Velde]

I'd start with rewriting hkn with docs#sub_eq_zero

[Damiano Testa]

Also, hN is probably unnecessary.

[Ruben Van de Velde]

And then I'd assume there's something about injectivity of that coercion, but I'm not seeing where the coercion to int is defined

[Damiano Testa]

h $ fin.coe_injective $ nat.cast_injective $ sub_eq_zero.mp hkn works, though I admit is very implicit...

[MohanadAhmed]

Thanks @Ruben Van de Velde

example {N : ℕ}
  {hN : 1 < N}
  (k n : fin N)
  (h : ¬k = n)
  (hkn : (↑k:ℤ) - ↑n = 0) :
  false :=
begin
  rw int.sub_eq_zero_iff_eq at hkn,
  simp only [coe_coe, nat.cast_inj] at *,
  rw fin.coe_eq_coe at hkn,
  exact h hkn,
end

[MohanadAhmed]

This one worked!

[Kevin Buzzard]

And indeed note that you never used hN, as you can easily see by deleting it and observing that the proof still works.

[MohanadAhmed]

Hello @Kevin Buzzard . Yes you are right!
Yeah this was the result of the extract_goal. The hN is needed in the next part where the complex exponential is not equal to 1.

[MohanadAhmed]

Damiano Testa said:

h $ fin.coe_injective $ nat.cast_injective $ sub_eq_zero.mp hkn works, though I admit is very implicit...

How do you read this statement?
Are the dollar signs separators?

Does it have the same meaning as in for example:

noncomputable def W_N {N: ℕ}: matrix (fin N) (fin N) ℂ :=
of $ λ k n,  exp(2 * π * I * k * n / N)

[Damiano Testa]

That is the very implicit term-mode proof.

The $ is equivalent to opening a parenthesis and letting Lean figure out the latest position where it can close it: it helps to remove long sequences of closed parentheses at the end of the line.

[Damiano Testa]

Essentially, f $ g $ h i means f (g (h i)).

[Damiano Testa]

I would read that statement as saying:

• apply h (like your last exact)
  [so now we are proving that k = n]

• After that, you apply a few injectivities of coercions (from fins to nats and from nats to ints)

• And you use the sub_eq_zero on your hypothesis with a subtraction.