map_nat_cast

Stream: maths

[Johan Commelin]

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]

It looks like eq_cast, but with the definition semiring_hom explicitly

[Johan Commelin]

Aha... I guess we want both versions?

[Johan Commelin]

And even better: ring_hom.map_nat_cast