Zulip Chat Archive

Stream: maths

Topic: ring_hom coe


view this post on Zulip Reid Barton (Oct 09 2019 at 21:28):

Is this missing? library_search failed

lemma ring_hom_coe {α β : Type} [comm_ring α] [comm_ring β] (f : α  β) [is_ring_hom f]
  (n : ) : f n = n :=
by library_search

view this post on Zulip Reid Barton (Oct 09 2019 at 21:28):

Oh wow I should look at the previous message in this stream.


Last updated: May 06 2021 at 17:38 UTC