Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-20 11:04 327259af

View on Github →

refactor(data/dfinsupp/basic): Improve definitional equalities of coercions (#15521) This means that dfinsupp.coe_add etc are true by definition, rather than requiring the application of quotient.induction first. The key change is that the underlying function is no longer "hidden" under the quotient, as it does not need to be. One motivation for this is to make the API more similar to that of finsupp. This change eliminates dfinsupp.pre, instead using {s : multiset ι // ∀ i, i ∈ s ∨ to_fun i = 0} directly. We no longer even need to create a setoid instance, since we can just use trunc. While adjusting some proofs in data/finsupp/interval to use the new definition, this ended up eliminating some decidable arguments. I don't think that is a consequence of this redefinition, and is incidental cleanup that could have been performed separately.

Estimated changes

added theorem dfinsupp.coe_mk'
deleted theorem dfinsupp.coe_pre_mk
modified theorem dfinsupp.coe_update
modified def dfinsupp.erase
modified def dfinsupp.extend_with
modified def dfinsupp.filter
modified def dfinsupp.map_range
deleted structure dfinsupp.pre
added theorem dfinsupp.to_fun_eq_coe
modified theorem dfinsupp.update_eq_erase
modified theorem dfinsupp.update_self
modified def dfinsupp.zip_with
added structure dfinsupp
deleted def dfinsupp