Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-29 13:24 8b858d0b

View on Github →

feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid (#3490) The extra _s required to make this still build are unfortunate, but hopefully someone else can work out how to remove them in a later PR.

Estimated changes