Zulip Chat Archive

Stream: maths

Topic: map_nat_cast


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 09 2019 at 09:18):

It looks like eq_cast, but with the definition semiring_hom explicitly

view this post on Zulip Johan Commelin (Oct 09 2019 at 09:20):

Aha... I guess we want both versions?

view this post on Zulip 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