ring_hom coe

Stream: maths

[Reid Barton]

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]

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