canonical ring hom from int to R

Stream: maths

[Johan Commelin]

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

[Kenny Lau]

something something int.coe

[Mario Carneiro]

int.cast

[Johan Commelin]

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

[Kenny Lau]

import data.int.basic

universe u

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

[Kenny Lau]

now you know

[Johan Commelin]

(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]

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

[Kevin Buzzard]

(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]

True, I keep forgetting that trick.

[Kevin Buzzard]

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]

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