Commit 2021-03-24 23:20 039dfd2e

View on Github →

refactor(data/finsupp): add decidable_eq (#6333) ... when the statement (not the proof) of the theorem depends on a decidability assumption. This prevents instance mismatch issues in downstream theorems.

Estimated changes

Modified src/data/finsupp/basic.lean

modified theorem finsupp.antidiagonal_support_filter_fst_eq

modified theorem finsupp.antidiagonal_support_filter_snd_eq

modified theorem finsupp.count_to_multiset

modified theorem finsupp.filter_apply

modified theorem finsupp.filter_eq_sum

modified theorem finsupp.map_domain_support

modified theorem finsupp.support_add

modified theorem finsupp.support_add_eq

modified theorem finsupp.support_curry

modified theorem finsupp.support_filter

modified theorem finsupp.support_subtype_domain

modified theorem finsupp.support_sum

modified theorem finsupp.support_zip_with

modified theorem finsupp.to_finset_to_multiset

modified theorem multiset.to_finsupp_apply

modified theorem multiset.to_finsupp_support

Modified src/data/mv_polynomial/basic.lean

modified theorem mv_polynomial.support_add

Modified src/data/polynomial/basic.lean

modified theorem polynomial.support_add

Modified src/logic/basic.lean