## Stream: maths

### Topic: int.cast is unique

#### Johan Commelin (Jan 21 2019 at 14:58):

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

#### Kevin Buzzard (Jan 21 2019 at 14:58):

I knew that, yes.

#### Johan Commelin (Jan 21 2019 at 14:59):

Did your Lean also know it?

#### Kevin Buzzard (Jan 21 2019 at 15:00):

Eew, is it some pretty grim induction?

#### Johan Commelin (Jan 21 2019 at 15:00):

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

#### Kevin Buzzard (Jan 21 2019 at 15:00):

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

#### Johan Commelin (Jan 21 2019 at 15:00):

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

#### Kevin Buzzard (Jan 21 2019 at 15:02):

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

#### Chris Hughes (Jan 21 2019 at 15:20):

int.eq_cast

#### 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