Theorem prod_indicator_const

Modification history

2024-10-27 19:58

Mathlib/Algebra/BigOperators/Pi.lean

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

Added prod_indicator_const View on Github →