mathlib3

114752ca - fix(algebra/monoid_algebra/basic): remove an instance that forms a diamond (#11918)

fix(algebra/monoid_algebra/basic): remove an instance that forms a diamond (#11918) This turns `monoid_algebra.comap_distrib_mul_action_self` from an instance to a def. This also adds some tests to prove that this diamond exists. Note that this diamond is not just non-defeq, it's also just plain not equal. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Schur's.20lemma/near/270990004)