Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-22 19:59 a0a21774

View on Github →

feat(data/support): add function.mul_support (#6791) This will help us add finprod in #6355

Estimated changes

Modified src/algebra/group/to_additive.lean

Modified src/data/support.lean

added theorem function.compl_mul_support

deleted theorem function.compl_support

added theorem function.mem_mul_support

deleted theorem function.mem_support

added def function.mul_support

added theorem function.mul_support_add_one'

added theorem function.mul_support_add_one

added theorem function.mul_support_binop_subset

added theorem function.mul_support_comp_eq

added theorem function.mul_support_comp_eq_preimage

added theorem function.mul_support_comp_subset

added theorem function.mul_support_div

added theorem function.mul_support_eq_empty_iff

added theorem function.mul_support_group_div

added theorem function.mul_support_inf

added theorem function.mul_support_infi

added theorem function.mul_support_inv''

added theorem function.mul_support_inv'

added theorem function.mul_support_inv

added theorem function.mul_support_max

added theorem function.mul_support_min

added theorem function.mul_support_mul

added theorem function.mul_support_mul_inv

added theorem function.mul_support_one'

added theorem function.mul_support_one

added theorem function.mul_support_one_add'

added theorem function.mul_support_one_add

added theorem function.mul_support_one_sub'

added theorem function.mul_support_one_sub

added theorem function.mul_support_prod

added theorem function.mul_support_prod_mk'

added theorem function.mul_support_prod_mk

added theorem function.mul_support_subset_comp

added theorem function.mul_support_subset_iff'

added theorem function.mul_support_subset_iff

added theorem function.mul_support_sup

added theorem function.mul_support_supr

added theorem function.nmem_mul_support

deleted theorem function.nmem_support

deleted theorem function.support_add

deleted theorem function.support_binop_subset

deleted theorem function.support_comp_eq

deleted theorem function.support_comp_eq_preimage

deleted theorem function.support_comp_subset

modified theorem function.support_div

deleted theorem function.support_eq_empty_iff

deleted theorem function.support_inf

deleted theorem function.support_infi

modified theorem function.support_inv

deleted theorem function.support_max

deleted theorem function.support_min

modified theorem function.support_mul

deleted theorem function.support_neg

deleted theorem function.support_prod_mk

modified theorem function.support_smul

modified theorem function.support_smul_subset_left

deleted theorem function.support_sub

deleted theorem function.support_subset_comp

deleted theorem function.support_subset_iff'

deleted theorem function.support_subset_iff

deleted theorem function.support_sum

deleted theorem function.support_sup

deleted theorem function.support_supr

deleted theorem function.support_zero'

deleted theorem function.support_zero

modified theorem pi.support_single_of_ne