Commit 2023-12-07 11:12 2016a40c

View on Github →

feat: When Finsupp.prod is nonzero (#8844) Also replace Finsupp.nonzero_iff_exists by a more general lemma.

Estimated changes

modified theorem DFinsupp.coe_mk'
modified theorem DFinsupp.coe_neg
modified theorem DFinsupp.coe_update
modified theorem DFinsupp.coe_zero
added theorem DFinsupp.ne_iff
deleted theorem DFinsupp.coeFn_mono
added theorem DFinsupp.coe_inf
added theorem DFinsupp.coe_le_coe
added theorem DFinsupp.coe_lt_coe
added theorem DFinsupp.coe_mono
added theorem DFinsupp.coe_sup
modified theorem DFinsupp.le_def
added theorem DFinsupp.lt_def
modified theorem Finsupp.coe_add
modified theorem Finsupp.coe_neg
modified theorem Finsupp.coe_sub
modified theorem Finsupp.coe_zero
added theorem Finsupp.ne_iff
added theorem Finsupp.coe_le_coe
added theorem Finsupp.coe_lt_coe
added theorem Finsupp.coe_mono
added theorem Finsupp.coe_strictMono
modified theorem Finsupp.coe_tsub
modified theorem Finsupp.le_def
added theorem Finsupp.lt_def
deleted theorem Finsupp.monotone_toFun