## Stream: maths

### Topic: map_nat_cast

#### Johan Commelin (Oct 09 2019 at 09:15):

I couldn't find the following in mathlib. Do we have it?

lemma map_nat_cast {α : Type*} {β : Type*} [semiring α] [semiring β]
(f : α → β) [is_semiring_hom f] (n : ℕ) :
f n = n :=
begin
induction n with n ih, { exact is_semiring_hom.map_zero f },
rw [nat.cast_succ, nat.cast_succ, is_semiring_hom.map_add f, ih, is_semiring_hom.map_one f],
end


#### Mario Carneiro (Oct 09 2019 at 09:18):

It looks like eq_cast, but with the definition semiring_hom explicitly

#### Johan Commelin (Oct 09 2019 at 09:20):

Aha... I guess we want both versions?

#### Johan Commelin (Oct 09 2019 at 09:20):

And even better: ring_hom.map_nat_cast

Last updated: May 14 2021 at 19:21 UTC