Commit 2024-03-12 22:32 1cf1beb7

View on Github →

chore (Multiset.Fintype): remove Multiset.coe_eq (#11340) This is now a rfl and in the latest nightly becomes a synTaut. We remove it.

Estimated changes

deleted theorem Multiset.coe_eq