has_map_add type class

Stream: maths

[Chris Hughes]

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]

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

[Chris Hughes]

Only like this rw has_map_add.map_add ℤ f,

[Yury G. Kudryashov]

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