Theorem Finset.mulIndicator_biUnion

Modification history

2024-11-29 02:34

Mathlib/Algebra/BigOperators/Group/Finset.lean

chore(Algebra/BigOperators/Group/Finset): golf some proofs (#19593)

Modified Finset.mulIndicator_biUnion View on Github →

2023-12-13 09:43

Mathlib/Algebra/BigOperators/Basic.lean

chore: Sink `Algebra.Support` down the import tree (#8919) …

Added Finset.mulIndicator_biUnion View on Github →