Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-15 01:31 4dbb3e23

View on Github →

chore(data/finsupp/basic): more lemmas about α →₀ ℕ (#5362)

define canonically_ordered_add_monoid instance;
add a few simp lemmas;
more lemmas about product over finsupp.antidiagonal n;
define finsupp.Iic_finset, use it for finite_le_nat.

Estimated changes

Modified src/data/finsupp/basic.lean

added def finsupp.Iic_finset

added theorem finsupp.antidiagonal_support_filter_fst_eq

added theorem finsupp.antidiagonal_support_filter_snd_eq

added theorem finsupp.coe_Iic_finset

added theorem finsupp.mem_Iic_finset

added theorem finsupp.nat_add_sub_cancel

added theorem finsupp.nat_add_sub_cancel_left

added theorem finsupp.nat_add_sub_of_le

added theorem finsupp.nat_sub_add_cancel

added theorem finsupp.nat_zero_sub

added theorem finsupp.prod_antidiagonal_support_swap

modified theorem finsupp.single_eq_zero

modified theorem finsupp.swap_mem_antidiagonal_support

Modified src/ring_theory/power_series.lean