Theorem Finset.dens_smul_finset

Modification history

2025-03-10 13:47
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean
chore: don't import Finset.Density in Group.Pointwise.Finset.Basic (#22480) …
Modified Finset.dens_smul_finsetView on Github →
2025-03-04 14:42
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean
chore: split off the action part of pointwise files (#22333) …
Modified Finset.dens_smul_finsetView on Github →
2024-09-22 15:36
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
feat(Finset): `(a • s).dens = s.dens` (#17020) …
Added Finset.dens_smul_finsetView on Github →