Zulip Chat Archive

Stream: maths

Topic: canonical ring hom from int to R


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 23 2018 at 06:56):

something something int.coe

view this post on Zulip Mario Carneiro (Jul 23 2018 at 06:57):

int.cast

view this post on Zulip Johan Commelin (Jul 23 2018 at 07:04):

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

view this post on Zulip 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_add := int.cast_add,
  map_mul := int.cast_mul,
  map_one := int.cast_one }

view this post on Zulip Kenny Lau (Jul 23 2018 at 07:14):

now you know

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:00):

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:22):

True, I keep forgetting that trick.

view this post on Zulip 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

view this post on Zulip 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