int * real

Stream: general

[James Arthur]

I am trying to prove that for a sine function every multiple of $\pi$ is 0. This is my code thus far:

import tactic
import basic zero_lemmas
import data.real.basic
import data.complex.exponential

lemma sin_npi (n : ℤ) : sin (n * pi) = 0 :=
begin
  {have H : 1 + (n-1) = n,
    {ring},
  rw [←H],
  have H2 : (1 + (n-1)) * pi = pi + (n - 1) * pi,

  sorry},

end

and get this error:

type mismatch at application
  (1 + (n - 1)) * pi
term
  pi
has type
  ℝ
but is expected to have type
  ℤ

I think it may be because I haven't imported the integers? As that was an issue before but I have tried to import:

import data.int.basic init.data.int.basic

but it still throws an error.

[Johan Commelin]

Lean sees 1 + (n - 1) and thinks you want to work with integers. You need to tell it explicitly that you want to view this as a real.

[Johan Commelin]

Telling lean to view x as a term of type Y can be done by writing (x : Y).

[Johan Commelin]

(This only works if someone explained to lean how to move x to this other type, this is called a coercion, or coe. Lean shows you that it coerced x by putting a tiny up-arrow before it.)

[James Arthur]

So I need something like this?

have H2 : ((1 + (n-1) : ℝ)) * pi = pi + (n - 1) * pi,

it works now but I fear that n is no longer an integer.

[Kevin Buzzard]

What do you mean "n is no longer an integer"? Things don't magically change their type. There are invisible functions in there. Look at the up arrows.

[James Arthur]

So even if I coerce $1 + (n-1)$ by using ((1 + (n-1) : ℝ)) , n is still an integer just that whole statement is a real? I see the arrows, they mean that the variable is in a different field to the rest doesn't it?

[Kevin Buzzard]

n is an integer and this won't ever change. \u n is a real. Coerce as soon as you can. Note that \u (n+1) isn't the same as (\u n) + 1 because those are two different addition functions. Compatible, but different.

[Kevin Buzzard]

norm_cast will try and write everything as \u (all the maths) and push_cast will try and write everything as (all the maths applied to \u stuff)

[James Arthur]

OK, that's very useful to know. I have now used the \u in the have and produced have H2 : (↑(1 + (n-1))) * pi = pi + (n - 1) * pi, . It now works, thanks!

[Bryan Gin-ge Chen]

By the way, I can't tell exactly since I don't know what's in basic and zero_lemmas, but there's something like sin_npi already proved in mathlib: src#real.sin_int_mul_pi

[Patrick Massot]

Elaborating on Bryan's comment: James, it's good that you tried to include the imports in the code you pasted, but they seem to refer to local files you have. The goal of this #mwe story is that people here can copy paste into their VScode and see your issue. Here we can't.

[James Arthur]

Sorry, I think the imports didn't explicitly import pi. I have worked everything out and moved my local imports away from the mathlib imports so that shouldn't happen again.