Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-28 17:54 3c02800d

View on Github →

chore(data/dfinsupp): use more precise decidable requirement (#2535) Removed decidable_zero_symm and replaced all [Π i, decidable_pred (eq (0 : β i))] with [Π i (x : β i), decidable (x ≠ 0)]. This should work better with open_locale classical because now the lemmas and definitions don't assume that [Π i (x : β i), decidable (x ≠ 0)] comes from decidable_zero_symm.

Estimated changes

deleted def decidable_zero_symm
modified theorem dfinsupp.eq_mk_support
modified theorem dfinsupp.map_range_def
modified def dfinsupp.prod
modified theorem dfinsupp.prod_add_index
modified theorem dfinsupp.prod_neg_index
modified theorem dfinsupp.prod_single_index
modified theorem dfinsupp.prod_zero_index
modified theorem dfinsupp.single_apply
modified theorem dfinsupp.smul_apply
modified theorem dfinsupp.sub_apply
modified theorem dfinsupp.subtype_domain_add
modified theorem dfinsupp.subtype_domain_neg
modified theorem dfinsupp.subtype_domain_sub
modified def dfinsupp.sum
modified theorem dfinsupp.sum_add
modified theorem dfinsupp.sum_neg
modified theorem dfinsupp.sum_sub_index
modified theorem dfinsupp.sum_zero
modified theorem dfinsupp.support_add
modified theorem dfinsupp.support_mk_subset
modified theorem dfinsupp.support_neg
modified def dfinsupp.to_module
modified def dfinsupp.zip_with
modified def dfinsupp