Commit 2024-03-31 21:48 6ed34ab6

View on Github →

chore(DFinsupp/Basic): drop a DecidableEq assumption (#11795) Golf DFinsupp.finite_support, drop an unneeded DecidableEq assumption.

Estimated changes

modified theorem DFinsupp.finite_support