Commit 2025-08-07 15:43 23a38dff

View on Github →

chore(Algebra/Notation): move Function.support earlier (#28064) The definition doesn't need anything about monoids/groups. This is useful to disentangle Finsupp results downstream.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean

Modified Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean

Modified Mathlib/Algebra/Group/FiniteSupport.lean

Modified Mathlib/Algebra/Group/Finsupp.lean

Modified Mathlib/Algebra/Group/Indicator.lean

Modified Mathlib/Algebra/Group/Support.lean

deleted theorem Function.compl_mulSupport

deleted theorem Function.disjoint_mulSupport_iff

deleted theorem Function.ext_iff_mulSupport

deleted theorem Function.mem_mulSupport

deleted def Function.mulSupport

deleted theorem Function.mulSupport_along_fiber_subset

deleted theorem Function.mulSupport_binop_subset

deleted theorem Function.mulSupport_comp_eq

deleted theorem Function.mulSupport_comp_eq_of_range_subset

deleted theorem Function.mulSupport_comp_eq_preimage

deleted theorem Function.mulSupport_comp_subset

deleted theorem Function.mulSupport_const

deleted theorem Function.mulSupport_curry

deleted theorem Function.mulSupport_disjoint_iff

deleted theorem Function.mulSupport_eq_empty_iff

deleted theorem Function.mulSupport_eq_iff

deleted theorem Function.mulSupport_eq_preimage

deleted theorem Function.mulSupport_extend_one

deleted theorem Function.mulSupport_extend_one_subset

deleted theorem Function.mulSupport_fun_curry

deleted theorem Function.mulSupport_fun_one

deleted theorem Function.mulSupport_nonempty_iff

deleted theorem Function.mulSupport_one

deleted theorem Function.mulSupport_prodMk'

deleted theorem Function.mulSupport_prodMk

deleted theorem Function.mulSupport_subset_comp

deleted theorem Function.mulSupport_subset_iff'

deleted theorem Function.mulSupport_subset_iff

deleted theorem Function.mulSupport_update_eq_ite

deleted theorem Function.mulSupport_update_of_ne_one

deleted theorem Function.mulSupport_update_one

deleted theorem Function.notMem_mulSupport

deleted theorem Function.range_eq_image_or_of_mulSupport_subset

deleted theorem Function.range_subset_insert_image_mulSupport

deleted theorem Pi.mulSupport_mulSingle

deleted theorem Pi.mulSupport_mulSingle_disjoint

deleted theorem Pi.mulSupport_mulSingle_of_ne

deleted theorem Pi.mulSupport_mulSingle_one

deleted theorem Pi.mulSupport_mulSingle_subset

deleted theorem Set.image_inter_mulSupport_eq

Modified Mathlib/Algebra/GroupWithZero/Indicator.lean

Created Mathlib/Algebra/Notation/Support.lean

added theorem Function.compl_mulSupport

added theorem Function.disjoint_mulSupport_iff

added theorem Function.ext_iff_mulSupport

added theorem Function.mem_mulSupport

added def Function.mulSupport

added theorem Function.mulSupport_along_fiber_subset

added theorem Function.mulSupport_binop_subset

added theorem Function.mulSupport_comp_eq

added theorem Function.mulSupport_comp_eq_of_range_subset

added theorem Function.mulSupport_comp_eq_preimage

added theorem Function.mulSupport_comp_subset

added theorem Function.mulSupport_const

added theorem Function.mulSupport_curry

added theorem Function.mulSupport_disjoint_iff

added theorem Function.mulSupport_eq_empty_iff

added theorem Function.mulSupport_eq_iff

added theorem Function.mulSupport_eq_preimage

added theorem Function.mulSupport_extend_one

added theorem Function.mulSupport_extend_one_subset

added theorem Function.mulSupport_fun_curry

added theorem Function.mulSupport_fun_one

added theorem Function.mulSupport_nonempty_iff

added theorem Function.mulSupport_one

added theorem Function.mulSupport_prodMk'

added theorem Function.mulSupport_prodMk

added theorem Function.mulSupport_subset_comp

added theorem Function.mulSupport_subset_iff'

added theorem Function.mulSupport_subset_iff

added theorem Function.mulSupport_update_eq_ite

added theorem Function.mulSupport_update_of_ne_one

added theorem Function.mulSupport_update_one

added theorem Function.notMem_mulSupport

added theorem Function.range_eq_image_or_of_mulSupport_subset

added theorem Function.range_subset_insert_image_mulSupport

added theorem Pi.mulSupport_mulSingle

added theorem Pi.mulSupport_mulSingle_disjoint

added theorem Pi.mulSupport_mulSingle_of_ne

added theorem Pi.mulSupport_mulSingle_one

added theorem Pi.mulSupport_mulSingle_subset

added theorem Set.image_inter_mulSupport_eq

Modified Mathlib/Algebra/Ring/CharZero.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Int/CharZero.lean

Modified Mathlib/Data/Set/Pointwise/Support.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/Topology/LocallyFinsupp.lean

Modified Mathlib/Topology/Separation/Basic.lean