Commit 2025-03-03 17:20 520bcc0a

View on Github →

chore(Data/Set/Pointwise/SMul): move content to earlier files (#20793) Move the content of Data.Set.Pointwise.SMul into three new files:

Algebra.Group.Action.Pointwise.Set for lemmas about monoids/groups
Algebra.GroupWithZero.Action.Pointwise.Set for lemmas about groups with zero. See https://github.com/leanprover-community/mathlib3/pull/11486 for the copyright header.
Algebra.Ring.Action.Pointwise.Set for lemmas about rings. See https://github.com/leanprover-community/mathlib3/pull/11486 for the copyright header.
Actually, there is a handful of lemmas that can simply be moved to existing earlier files.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Data/Set/Pointwise/SMul.lean to Mathlib/Algebra/Group/Action/Pointwise/Set.lean

deleted theorem Set.Nonempty.smul_zero

deleted theorem Set.Nonempty.zero_smul

deleted theorem Set.add_smul_subset

modified theorem Set.image_smul_distrib

deleted theorem Set.inv_op_smul_set_distrib₀

deleted theorem Set.inv_smul_set_distrib₀

deleted theorem Set.mem_inv_smul_set_iff₀

deleted theorem Set.mem_smul_set_iff_inv_smul_mem₀

deleted theorem Set.neg_smul_set

modified theorem Set.op_smul_set_mul_eq_mul_smul_set

deleted theorem Set.op_smul_set_smul_eq_smul_smul_set

deleted theorem Set.preimage_smul_inv₀

deleted theorem Set.preimage_smul₀

modified theorem Set.range_mul

deleted theorem Set.smul_mem_smul_set_iff₀

deleted theorem Set.smul_set_inter₀

deleted theorem Set.smul_set_neg

modified theorem Set.smul_set_pi

modified theorem Set.smul_set_pi_of_isUnit

deleted theorem Set.smul_set_pi₀

modified theorem Set.smul_set_prod

deleted theorem Set.smul_set_sdiff₀

deleted theorem Set.smul_set_subset_iff₀

deleted theorem Set.smul_set_subset_smul_set_iff₀

deleted theorem Set.smul_set_symmDiff₀

deleted theorem Set.smul_set_univ₀

deleted theorem Set.smul_univ₀'

deleted theorem Set.smul_univ₀

deleted theorem Set.smul_zero_subset

deleted theorem Set.subset_smul_set_iff₀

deleted theorem Set.subsingleton_zero_smul_set

deleted theorem Set.zero_mem_smul_iff

deleted theorem Set.zero_mem_smul_set

deleted theorem Set.zero_mem_smul_set_iff

deleted theorem Set.zero_smul_set

deleted theorem Set.zero_smul_set_subset

deleted theorem Set.zero_smul_subset

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

added theorem Set.op_smul_set_smul_eq_smul_smul_set

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

Modified Mathlib/Algebra/Group/Translate.lean

Created Mathlib/Algebra/GroupWithZero/Action/Pointwise/Set.lean

added theorem Set.Nonempty.smul_zero

added theorem Set.Nonempty.zero_smul

added theorem Set.inv_op_smul_set_distrib₀

added theorem Set.inv_smul_set_distrib₀

added theorem Set.mem_inv_smul_set_iff₀

added theorem Set.mem_smul_set_iff_inv_smul_mem₀

added theorem Set.preimage_smul_inv₀

added theorem Set.preimage_smul₀

added theorem Set.smul_mem_smul_set_iff₀

added theorem Set.smul_set_inter₀

added theorem Set.smul_set_pi₀

added theorem Set.smul_set_sdiff₀

added theorem Set.smul_set_subset_iff₀

added theorem Set.smul_set_subset_smul_set_iff₀

added theorem Set.smul_set_symmDiff₀

added theorem Set.smul_set_univ₀

added theorem Set.smul_univ₀'

added theorem Set.smul_univ₀

added theorem Set.smul_zero_subset

added theorem Set.subset_smul_set_iff₀

added theorem Set.subsingleton_zero_smul_set

added theorem Set.zero_mem_smul_iff

added theorem Set.zero_mem_smul_set

added theorem Set.zero_mem_smul_set_iff

added theorem Set.zero_smul_set

added theorem Set.zero_smul_set_subset

added theorem Set.zero_smul_subset

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

Modified Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean

Modified Mathlib/Algebra/Module/PointwisePi.lean

Modified Mathlib/Algebra/Order/UpperLower.lean

Created Mathlib/Algebra/Ring/Action/Pointwise/Set.lean

added theorem Set.add_smul_subset

added theorem Set.neg_smul_set

added theorem Set.smul_set_neg

Modified Mathlib/Algebra/Ring/Pointwise/Finset.lean

Modified Mathlib/Algebra/Ring/Pointwise/Set.lean

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/Analysis/Convex/Star.lean

Modified Mathlib/Data/Real/Pointwise.lean

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

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

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coset/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/FixedPoints.lean

Modified Mathlib/LinearAlgebra/Span/Basic.lean

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/RingTheory/Ideal/Colon.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

Modified Mathlib/Topology/Algebra/Ring/Basic.lean

Modified Mathlib/Topology/Bornology/Absorbs.lean

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean