Commit 2024-08-01 16:59 f05779eb
View on Github →chore: remove unnecessary implicit arguments in MonoidWithZeroHom.coe_copy (#15248) It's perfectly fine for these to just be instance implicit arguments.
chore: remove unnecessary implicit arguments in MonoidWithZeroHom.coe_copy (#15248) It's perfectly fine for these to just be instance implicit arguments.