Commit 2023-02-05 11:33 adaaf293

View on Github →

fix: use to_additive (attr := _) here and there (#2073)

Estimated changes

modified def MonoidHom.coeFn
modified def MulHom.single
modified def OneHom.single
modified def Pi.constMonoidHom
modified def Pi.evalMonoidHom
modified def Units.embedProduct
modified def divMonoidHom
modified def divMonoidWithZeroHom
deleted theorem AddEquiv.neg_apply
modified theorem MulEquiv.inv_apply
modified def Finset.imageMulHom
modified def FreeGroup.lift
modified theorem Equiv.mulLeft_mul
modified theorem Equiv.mulLeft_one
modified theorem Equiv.mulRight_mul
modified theorem Equiv.mulRight_one