Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-18 01:46 f9908388

View on Github →

chore(data/finsupp/basic): rename type variables (#4624) Use M, N, P for types with has_zero, add_monoid, or add_comm_monoid structure, and R, S for types with at least a semiring instance. API change: single_add_erase and erase_add_single now use explicit arguments.

Estimated changes

modified theorem finsupp.add_apply
modified theorem finsupp.add_eq_zero_iff
modified theorem finsupp.add_hom_ext
modified def finsupp.antidiagonal
modified theorem finsupp.antidiagonal_zero
modified theorem finsupp.card_support_eq_one
modified theorem finsupp.coe_leval'
modified theorem finsupp.coe_leval
modified def finsupp.comap_domain
modified theorem finsupp.comap_domain_apply
modified theorem finsupp.comap_smul_apply
modified theorem finsupp.comap_smul_single
modified def finsupp.emb_domain
modified theorem finsupp.emb_domain_apply
modified theorem finsupp.emb_domain_eq_zero
modified theorem finsupp.emb_domain_inj
modified theorem finsupp.emb_domain_zero
modified theorem finsupp.eq_single_iff
modified def finsupp.erase
modified theorem finsupp.erase_add
modified theorem finsupp.erase_add_single
modified theorem finsupp.erase_ne
modified theorem finsupp.erase_same
modified theorem finsupp.erase_single
modified theorem finsupp.erase_single_ne
modified theorem finsupp.erase_zero
modified def finsupp.eval_add_hom
modified theorem finsupp.eval_add_hom_apply
modified theorem finsupp.ext
modified theorem finsupp.ext_iff
modified def finsupp.filter
modified theorem finsupp.filter_add
modified theorem finsupp.filter_curry
modified theorem finsupp.filter_smul
modified theorem finsupp.filter_sum
modified theorem finsupp.filter_zero
modified theorem finsupp.finite_le_nat
modified theorem finsupp.finite_lt_nat
modified theorem finsupp.finite_supp
modified def finsupp.frange
modified theorem finsupp.frange_single
modified theorem finsupp.induction₂
modified theorem finsupp.le_iff
modified def finsupp.leval'
modified def finsupp.leval
modified theorem finsupp.lhom_ext'
modified theorem finsupp.lhom_ext
modified def finsupp.lift_add_hom
modified theorem finsupp.lift_add_hom_apply
modified theorem finsupp.lt_wf
modified def finsupp.map_domain
modified theorem finsupp.map_domain_add
modified theorem finsupp.map_domain_apply
modified theorem finsupp.map_domain_comp
modified theorem finsupp.map_domain_congr
modified theorem finsupp.map_domain_single
modified theorem finsupp.map_domain_smul
modified theorem finsupp.map_domain_sum
modified theorem finsupp.map_domain_support
modified theorem finsupp.map_domain_zero
modified def finsupp.map_range
modified theorem finsupp.map_range_add
modified theorem finsupp.map_range_apply
modified theorem finsupp.map_range_single
modified theorem finsupp.map_range_zero
modified theorem finsupp.mem_frange
modified theorem finsupp.mem_support_iff
modified theorem finsupp.mem_support_single
modified theorem finsupp.mul_sum
modified theorem finsupp.multiset_map_sum
modified theorem finsupp.multiset_sum_sum
modified theorem finsupp.neg_apply
modified theorem finsupp.not_mem_support_iff
modified def finsupp.on_finset
modified theorem finsupp.on_finset_apply
modified theorem finsupp.on_finset_sum
modified def finsupp.prod
modified theorem finsupp.prod_add_index
modified theorem finsupp.prod_comm
modified theorem finsupp.prod_emb_domain
modified theorem finsupp.prod_fintype
added theorem finsupp.prod_inv
modified theorem finsupp.prod_ite_eq'
modified theorem finsupp.prod_ite_eq
added theorem finsupp.prod_mul
modified theorem finsupp.prod_neg_index
modified theorem finsupp.prod_pow
modified theorem finsupp.prod_single_index
modified theorem finsupp.prod_to_multiset
modified theorem finsupp.prod_zero_index
modified theorem finsupp.sigma_sum
modified def finsupp.single
modified theorem finsupp.single_add
modified theorem finsupp.single_add_erase
modified theorem finsupp.single_apply
modified theorem finsupp.single_eq_of_ne
modified theorem finsupp.single_eq_same
modified theorem finsupp.single_finset_sum
modified theorem finsupp.single_injective
modified theorem finsupp.single_multiset_sum
modified theorem finsupp.single_sum
modified theorem finsupp.single_swap
modified theorem finsupp.single_zero
modified theorem finsupp.smul_apply'
modified theorem finsupp.smul_apply
modified theorem finsupp.smul_single'
modified theorem finsupp.smul_single
modified theorem finsupp.smul_single_one
modified def finsupp.split
modified def finsupp.split_comp
modified theorem finsupp.sub_apply
modified theorem finsupp.subtype_domain_add
modified theorem finsupp.subtype_domain_neg
modified theorem finsupp.subtype_domain_sub
modified theorem finsupp.subtype_domain_sum
modified theorem finsupp.subtype_domain_zero
modified def finsupp.sum
deleted theorem finsupp.sum_add
modified theorem finsupp.sum_apply
modified theorem finsupp.sum_comap_domain
modified theorem finsupp.sum_curry_index
modified theorem finsupp.sum_id_lt_of_lt
modified theorem finsupp.sum_mul
deleted theorem finsupp.sum_neg
modified theorem finsupp.sum_single
modified theorem finsupp.sum_smul_index'
modified theorem finsupp.sum_smul_index
modified theorem finsupp.sum_sub
modified theorem finsupp.sum_zero
modified theorem finsupp.support_add
modified theorem finsupp.support_add_eq
modified theorem finsupp.support_curry
modified theorem finsupp.support_emb_domain
modified theorem finsupp.support_eq_empty
modified theorem finsupp.support_erase
modified theorem finsupp.support_map_range
modified theorem finsupp.support_neg
modified theorem finsupp.support_smul
modified theorem finsupp.support_subset_iff
modified theorem finsupp.support_sum
modified theorem finsupp.support_zero
modified theorem finsupp.support_zip_with
modified theorem finsupp.unique_ext
modified theorem finsupp.unique_ext_iff
modified theorem finsupp.unique_single
modified theorem finsupp.zero_apply
modified theorem finsupp.zero_not_mem_frange
modified def finsupp.zip_with
modified structure finsupp
modified theorem monoid_hom.map_finsupp_prod
modified theorem mul_equiv.map_finsupp_prod
modified theorem ring_hom.map_finsupp_prod
modified theorem ring_hom.map_finsupp_sum