Commit 2026-02-04 17:03 73694cf6

feat: clean up Mul -> FaithfulSMul instance structure (#34789) Given MulOneClass A, the induced smultiplications SMul A A and SMul (MulOpposite A) A are faithful. As a result, the same holds when given RightCancelMonoid A, LeftCancelMonoid A or RightCancelMonoidWithZero A. the instances representing the latter three facts are removed due to their redundancy. (Also for the to_additive versions when applicable.) Secondly, given Mul A, and given IsRightCancelMul A or IsLeftCancelMul A, we find that SMul A A or SMul (MulOpposite A) A is faithful, respectively. The instances representing these facts are added.