int.cast is unique

Stream: maths

[Johan Commelin]

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

[Kevin Buzzard]

I knew that, yes.

[Johan Commelin]

Did your Lean also know it?

[Kevin Buzzard]

Eew, is it some pretty grim induction?

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

int.eq_cast

[Johan Commelin]

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