Commit 2025-03-10 13:47 113f4fe9

View on Github →

chore: don't import Finset.Density in Group.Pointwise.Finset.Basic (#22480) Minor effect, but this was getting in the way while looking at other splits.

Estimated changes

Modified Mathlib.lean

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

deleted theorem Finset.dens_smul_finset

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

deleted theorem Finset.dens_inv

Created Mathlib/Algebra/Group/Pointwise/Finset/Density.lean

added theorem Finset.dens_inv

added theorem Finset.dens_smul_finset

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

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

Modified Mathlib/Algebra/Pointwise/Stabilizer.lean

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

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/RingTheory/WittVector/WittPolynomial.lean