Commit 2024-10-27 19:58 64e38517

View on Github →

feat: a product of indicators is the indicator of the product (#17964)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Pi.lean

added theorem prod_indicator

added theorem prod_indicator_apply

added theorem prod_indicator_const

added theorem prod_indicator_const_apply

Modified Mathlib/Algebra/BigOperators/Ring.lean

added theorem Finset.prod_sub

Modified Mathlib/Data/Finset/Lattice.lean

added theorem Finset.mem_inf'

added theorem Finset.mem_sup'

modified theorem Finset.mem_sup

modified theorem Finset.sup_singleton''

modified theorem Finset.sup_singleton'