Zulip Chat Archive

Stream: maths

Topic: int.cast is unique


view this post on Zulip Johan Commelin (Jan 21 2019 at 14:58):

Do we already know that int.cast is the unique ring hom ℤ → R?

view this post on Zulip Kevin Buzzard (Jan 21 2019 at 14:58):

I knew that, yes.

view this post on Zulip Johan Commelin (Jan 21 2019 at 14:59):

Did your Lean also know it?

view this post on Zulip Kevin Buzzard (Jan 21 2019 at 15:00):

Eew, is it some pretty grim induction?

view this post on Zulip Johan Commelin (Jan 21 2019 at 15:00):

I don't know, I just want to use it if it's in mathlib.

view this post on Zulip Kevin Buzzard (Jan 21 2019 at 15:00):

Yes, I don't think I've seen my Lean know it...

view this post on Zulip Johan Commelin (Jan 21 2019 at 15:00):

I can probably write a proof in a couple of minutes...

view this post on Zulip Kevin Buzzard (Jan 21 2019 at 15:02):

If we have two ring homomorphisms from AA to BB then the subset of AA where they coincide is a subring. Do we know that Z\mathbb{Z} has no subrings other than itself?

view this post on Zulip Chris Hughes (Jan 21 2019 at 15:20):

int.eq_cast

view this post on Zulip Johan Commelin (Jan 21 2019 at 15:23):

Aah... nice. Too bad it isn't stated in terms of ring homs.


Last updated: May 06 2021 at 18:20 UTC