Commit 2025-01-24 22:23 a7b7802c

View on Github →

chore(Pointwise): rename Set.set_smul_subset_set_smul_iff to Set.smul_set_subset_smul_set_iff (#20300) Moves:

set_smul_subset_set_smul_iff → smul_set_subset_smul_set_iff
set_smul_subset_iff → smul_set_subset_iff_subset_inv_smul_set
subset_set_smul_iff → subset_smul_set_iff
set_smul_subset_set_smul_iff₀ → smul_set_subset_smul_set_iff₀
set_smul_subset_iff₀ → smul_set_subset_iff₀
subset_set_smul_iff₀ → subset_smul_set_iff₀ From LeanCamCombi

Estimated changes

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

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

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

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

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

Modified Mathlib/Analysis/Convex/Normed.lean

Modified Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

Modified Mathlib/Analysis/Normed/Operator/Compact.lean

Modified Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean

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

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

deleted theorem Set.set_smul_subset_iff

deleted theorem Set.set_smul_subset_iff₀

deleted theorem Set.set_smul_subset_set_smul_iff

deleted theorem Set.set_smul_subset_set_smul_iff₀

added theorem Set.smul_set_subset_iff_subset_inv_smul_set

added theorem Set.smul_set_subset_iff₀

added theorem Set.smul_set_subset_smul_set_iff

added theorem Set.smul_set_subset_smul_set_iff₀

deleted theorem Set.subset_set_smul_iff

deleted theorem Set.subset_set_smul_iff₀

added theorem Set.subset_smul_set_iff

added theorem Set.subset_smul_set_iff₀

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Modified Mathlib/GroupTheory/GroupAction/FixedPoints.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean