Zulip Chat Archive

Stream: maths

Topic: ring_hom coe


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

Reid Barton (Oct 09 2019 at 21:28):

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


Last updated: Dec 20 2023 at 11:08 UTC