mathlib

1dddd7f9 - feat(algebra/group/hom_instance): additive endomorphisms form a ring (#8954)

feat(algebra/group/hom_instance): additive endomorphisms form a ring (#8954) We already have all the data to state this, this just provides the extra proofs. The multiplicative version is nasty because `monoid.End` has two different multiplicative structures depending on whether `End` is unfolded; so this PR leaves that until someone actually needs it. With this in place we can provide `module.to_add_monoid_End : R →+* add_monoid.End M` in a future PR.