## Stream: general

### Topic: int * real

#### James Arthur (Jul 01 2020 at 08:14):

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 (Jul 01 2020 at 08:15):

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 (Jul 01 2020 at 08:16):

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

#### Johan Commelin (Jul 01 2020 at 08:17):

(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 (Jul 01 2020 at 08:20):

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 (Jul 01 2020 at 08:20):

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 (Jul 01 2020 at 08:23):

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 (Jul 01 2020 at 08:26):

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 (Jul 01 2020 at 08:27):

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 (Jul 01 2020 at 08:27):

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 (Jul 01 2020 at 08:28):

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 (Jul 01 2020 at 08:29):

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 (Jul 01 2020 at 08:33):

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.

Last updated: May 11 2021 at 13:22 UTC