Commit 2023-08-18 23:14 fd3a26ed

View on Github →

fix(Algebra/IndicatorFunction): minor fixes (#6640)

Fix name in docstrings.
Use Type* in variable, explicitly use Sort*.
Use to_additive to generate the additive version.
Drop pattern matching.
Add Set.mulIndicator_diff', the multiplicative version of Set.indicator_diff.

Estimated changes

Modified Mathlib/Algebra/IndicatorFunction.lean

deleted theorem Set.indicator_compl

deleted theorem Set.indicator_diff

added theorem Set.mulIndicator_compl'

added theorem Set.mulIndicator_diff'

modified theorem Set.mulIndicator_finset_biUnion

modified theorem Set.mulIndicator_finset_biUnion_apply

modified theorem Set.mulIndicator_iInter_apply

modified theorem Set.mulIndicator_iUnion_apply