## Stream: general

### Topic: missing simp lemmas?

#### Johan Commelin (Feb 11 2019 at 09:05):

Shouldn't these be simp lemmas?

namespace is_ring_hom
variables {β : Type v} [ring α] [ring β]
variables (f : α → β) [is_ring_hom f] {x y : α}

lemma map_zero : f 0 = 0 :=
calc f 0 = f (0 + 0) - f 0 : by rw [map_add f]; simp
... = 0 : by simp

lemma map_neg : f (-x) = -f x :=
calc f (-x) = f (-x + x) - f x : by rw [map_add f]; simp
... = -f x : by simp [map_zero f]

lemma map_sub : f (x - y) = f x - f y :=
by simp [map_add f, map_neg f]


won't work

#### Mario Carneiro (Feb 11 2019 at 09:06):

If ring_hom becomes a type then these can be simp lemmas

Too bad...

#### Kevin Buzzard (Feb 11 2019 at 09:21):

You could make them typeclasses ;-)

#### Mario Carneiro (Feb 11 2019 at 09:26):

huh? it's already a typeclass

#### Wojciech Nawrocki (Feb 11 2019 at 16:40):

Why wouldn't this work? Can simp not match a type class when looking up lemmas?

#### Kevin Buzzard (Feb 11 2019 at 16:43):

I mean map_zero_class etc :-) Then type class inference could do it, right?

#### Reid Barton (Feb 11 2019 at 16:47):

It can't match a rule where the left-hand side is the application of a variable function. Or so I've gathered.

#### Reid Barton (Feb 11 2019 at 16:47):

Here, f

Last updated: May 13 2021 at 05:21 UTC