Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-25 03:23 c3034c27

View on Github →

feat(data/indicator_function): add multiplicative version (#6794) We need it for finprod

Estimated changes

Modified src/algebra/group/to_additive.lean

Modified src/data/indicator_function.lean

deleted theorem add_monoid_hom.map_indicator

added theorem monoid_hom.map_mul_indicator

deleted theorem set.comp_indicator

added theorem set.comp_mul_indicator

deleted theorem set.eq_on_indicator

added theorem set.eq_on_mul_indicator

modified def set.indicator

deleted theorem set.indicator_Union_apply

deleted theorem set.indicator_add

deleted theorem set.indicator_add_eq_left

deleted theorem set.indicator_add_eq_right

deleted theorem set.indicator_apply

deleted theorem set.indicator_apply_eq_self

deleted theorem set.indicator_apply_eq_zero

deleted theorem set.indicator_comp_of_zero

deleted theorem set.indicator_comp_right

modified theorem set.indicator_compl

deleted theorem set.indicator_compl_add_self

deleted theorem set.indicator_compl_add_self_apply

deleted theorem set.indicator_congr

deleted theorem set.indicator_empty

deleted theorem set.indicator_eq_self

deleted theorem set.indicator_eq_self_of_superset

deleted theorem set.indicator_eq_zero'

deleted theorem set.indicator_eq_zero

deleted theorem set.indicator_eq_zero_or_self

deleted theorem set.indicator_finset_bUnion

deleted theorem set.indicator_finset_sum

deleted theorem set.indicator_indicator

deleted theorem set.indicator_le'

deleted theorem set.indicator_le

deleted theorem set.indicator_le_indicator

deleted theorem set.indicator_le_indicator_of_subset

deleted theorem set.indicator_le_self'

deleted theorem set.indicator_le_self

modified theorem set.indicator_mul

modified theorem set.indicator_mul_left

modified theorem set.indicator_mul_right

deleted theorem set.indicator_neg

deleted theorem set.indicator_nonneg'

deleted theorem set.indicator_nonneg

deleted theorem set.indicator_nonpos'

deleted theorem set.indicator_nonpos

deleted theorem set.indicator_of_mem

deleted theorem set.indicator_of_not_mem

deleted theorem set.indicator_preimage

deleted theorem set.indicator_preimage_of_not_mem

modified theorem set.indicator_prod_one

deleted theorem set.indicator_range_comp

deleted theorem set.indicator_rel_indicator

deleted theorem set.indicator_self_add_compl

deleted theorem set.indicator_self_add_compl_apply

modified theorem set.indicator_smul

modified theorem set.indicator_sub

deleted theorem set.indicator_support

deleted theorem set.indicator_union_of_disjoint

deleted theorem set.indicator_union_of_not_mem_inter

deleted theorem set.indicator_univ

deleted theorem set.indicator_zero'

deleted theorem set.indicator_zero

modified theorem set.inter_indicator_mul

added theorem set.le_mul_indicator

added theorem set.le_mul_indicator_apply

deleted theorem set.mem_of_indicator_ne_zero

added theorem set.mem_of_mul_indicator_ne_one

deleted theorem set.mem_range_indicator

added theorem set.mem_range_mul_indicator

added def set.mul_indicator

added theorem set.mul_indicator_Union_apply

added theorem set.mul_indicator_apply

added theorem set.mul_indicator_apply_eq_one

added theorem set.mul_indicator_apply_eq_self

added theorem set.mul_indicator_apply_le'

added theorem set.mul_indicator_apply_le

added theorem set.mul_indicator_apply_le_one

added theorem set.mul_indicator_comp_of_one

added theorem set.mul_indicator_comp_right

added theorem set.mul_indicator_compl

added theorem set.mul_indicator_compl_mul_self

added theorem set.mul_indicator_compl_mul_self_apply

added theorem set.mul_indicator_congr

added theorem set.mul_indicator_empty

added theorem set.mul_indicator_eq_one'

added theorem set.mul_indicator_eq_one

added theorem set.mul_indicator_eq_one_or_self

added theorem set.mul_indicator_eq_self

added theorem set.mul_indicator_eq_self_of_superset

added theorem set.mul_indicator_finset_bUnion

added theorem set.mul_indicator_finset_prod

added def set.mul_indicator_hom

added theorem set.mul_indicator_inter_mul_support

added theorem set.mul_indicator_inv'

added theorem set.mul_indicator_inv

added theorem set.mul_indicator_le'

added theorem set.mul_indicator_le

added theorem set.mul_indicator_le_mul_indicator

added theorem set.mul_indicator_le_mul_indicator_of_subset

added theorem set.mul_indicator_le_one

added theorem set.mul_indicator_le_self'

added theorem set.mul_indicator_le_self

added theorem set.mul_indicator_mul

added theorem set.mul_indicator_mul_eq_left

added theorem set.mul_indicator_mul_eq_right

added theorem set.mul_indicator_mul_indicator

added theorem set.mul_indicator_mul_support

added theorem set.mul_indicator_of_mem

added theorem set.mul_indicator_of_not_mem

added theorem set.mul_indicator_one'

added theorem set.mul_indicator_one

added theorem set.mul_indicator_preimage

added theorem set.mul_indicator_preimage_of_not_mem

added theorem set.mul_indicator_range_comp

added theorem set.mul_indicator_rel_mul_indicator

added theorem set.mul_indicator_self_mul_compl

added theorem set.mul_indicator_self_mul_compl_apply

added theorem set.mul_indicator_union_mul_inter

added theorem set.mul_indicator_union_mul_inter_apply

added theorem set.mul_indicator_union_of_disjoint

added theorem set.mul_indicator_union_of_not_mem_inter

added theorem set.mul_indicator_univ

added theorem set.mul_support_mul_indicator

added theorem set.mul_support_mul_indicator_subset

added theorem set.one_le_mul_indicator

added theorem set.one_le_mul_indicator_apply

deleted theorem set.piecewise_eq_indicator

added theorem set.piecewise_eq_mul_indicator

added theorem set.prod_mul_indicator_subset

added theorem set.prod_mul_indicator_subset_of_eq_one

deleted theorem set.sum_indicator_subset

deleted theorem set.sum_indicator_subset_of_eq_zero

deleted theorem set.support_indicator

deleted theorem set.support_indicator_subset

Modified src/data/support.lean

Modified src/measure_theory/integration.lean

Modified src/measure_theory/measurable_space.lean

added theorem measurable_set_mul_support

Modified src/measure_theory/outer_measure.lean

Modified src/measure_theory/set_integral.lean

added theorem measure_theory.integrable.indicator