Commit 2025-08-13 18:45 0bdc4bfb

View on Github →

chore(Algebra/Notation): separate very basic lemmas about Set.indicator (#24998) The very basic lemmas go under Algebra.Notation and do not import Monoid. Also Pi.prod, which doesn't look like it belongs anywhere specific. This is useful to disentangle Finsupp results downstream.

Estimated changes

deleted theorem Set.comp_mulIndicator
deleted theorem Set.eqOn_mulIndicator'
deleted theorem Set.eqOn_mulIndicator
deleted theorem Set.mulIndicator_apply
deleted theorem Set.mulIndicator_congr
deleted theorem Set.mulIndicator_empty'
deleted theorem Set.mulIndicator_empty
deleted theorem Set.mulIndicator_eq_one'
deleted theorem Set.mulIndicator_eq_one
deleted theorem Set.mulIndicator_eq_self
deleted theorem Set.mulIndicator_image
deleted theorem Set.mulIndicator_of_mem
deleted theorem Set.mulIndicator_one'
deleted theorem Set.mulIndicator_one
deleted theorem Set.mulIndicator_preimage
deleted theorem Set.mulIndicator_univ
deleted theorem Pi.prod_fst_snd
deleted theorem Pi.prod_snd_fst
added theorem Set.comp_mulIndicator
added theorem Set.eqOn_mulIndicator'
added theorem Set.eqOn_mulIndicator
added theorem Set.mulIndicator_apply
added theorem Set.mulIndicator_congr
added theorem Set.mulIndicator_empty
added theorem Set.mulIndicator_image
added theorem Set.mulIndicator_one'
added theorem Set.mulIndicator_one
added theorem Set.mulIndicator_univ
added theorem Pi.prod_fst_snd
added theorem Pi.prod_snd_fst