Commit 2020-12-10 23:19 918d5a95

View on Github →

chore(data/finsupp/basic): redefine finsupp.filter (#5310) Also use lemmas about indicator_function and function.update to golf some proofs about finsupp.single.

Estimated changes

Modified src/data/finsupp/basic.lean

modified theorem finsupp.add_apply

added theorem finsupp.coe_add

added theorem finsupp.coe_fn_injective

modified theorem finsupp.ext

modified theorem finsupp.filter_add

added def finsupp.filter_add_hom

added theorem finsupp.filter_apply

added theorem finsupp.filter_eq_indicator

added theorem finsupp.filter_eq_sum

added theorem finsupp.fun_support_eq

deleted theorem finsupp.injective_coe_fn

modified theorem finsupp.single_apply

added theorem finsupp.single_apply_eq_zero

added theorem finsupp.single_eq_indicator

added theorem finsupp.single_eq_update

modified theorem finsupp.support_filter

Modified src/data/polynomial/degree/trailing_degree.lean