## Stream: maths

#### Chris Hughes (Jul 20 2019 at 09:32):

I thought it might be a good idea to create a has_map_add type class, and prove that ring_homs and add_group_homs were instances of this, and define the simp lemmas on the has_map_add type class, but I couldn't get it to work. https://gist.github.com/ChrisHughes24/e18d1a47592b23f1f7bc6ada7ffd2bb9

Can something like this be made to work ever? Is it a good idea?

#### Kevin Buzzard (Jul 20 2019 at 09:59):

Mathematically this looks like a natural idea! The simp doesn't work? Can you rw map_add?

#### Chris Hughes (Jul 20 2019 at 10:01):

Only like this rw has_map_add.map_add ℤ f,

#### Yury G. Kudryashov (Jul 21 2019 at 07:49):

Why this is better than making is_ring_hom extend is_add_hom? Or you're talking about bundled homs?

Last updated: May 10 2021 at 08:14 UTC