## Stream: maths

### Topic: canonical ring hom from int to R

#### Johan Commelin (Jul 23 2018 at 06:56):

Does the canonical ring homomorphism from int to a ring R already have a name in Lean?

#### Kenny Lau (Jul 23 2018 at 06:56):

something something int.coe

#### Mario Carneiro (Jul 23 2018 at 06:57):

int.cast

#### Johan Commelin (Jul 23 2018 at 07:04):

Aah, of course. And do we already know that this is a ring hom?

#### Kenny Lau (Jul 23 2018 at 07:14):

import data.int.basic

universe u

instance int.cast.is_ring_hom (α : Type u) [ring α] : is_ring_hom (int.cast : ℤ → α) :=
map_mul := int.cast_mul,
map_one := int.cast_one }


now you know

#### Johan Commelin (Jul 23 2018 at 07:58):

(Sorry, I got distracted by other stuff.) Anyway, I'm not surprised that it is a 4-liner. It is just that I don't know how to figure out if this is somewhere in mathlib or not...

#### Mario Carneiro (Jul 23 2018 at 08:00):

it is not, but kenny is pointing out that all the theorems are already there

#### Kevin Buzzard (Jul 23 2018 at 08:19):

(Sorry, I got distracted by other stuff.) Anyway, I'm not surprised that it is a 4-liner. It is just that I don't know how to figure out if this is somewhere in mathlib or not...

You can check to see if Lean's type class inference system already knows a fact by seeing if you can prove it with by apply_instance. Of course this does not tell you whether the proof is in mathlib in a file you didn't import yet...

#### Johan Commelin (Jul 23 2018 at 08:22):

True, I keep forgetting that trick.

#### Kevin Buzzard (Jul 23 2018 at 08:50):

I used it extensively over the weekend in the middle of code just to make sure that type class inference was keeping up with what I was trying to do

#### Kevin Buzzard (Jul 23 2018 at 08:51):

Just debugging lines which I'd delete after, checking my quotient group instances were working

Last updated: May 19 2021 at 02:10 UTC