Theorem Finset.image_smul_distrib

Modification history

2025-03-29 10:26
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean
feat: generalize Mathlib.Algebra.Group+Ring+Field (#23143) …
Modified Finset.image_smul_distribView 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.image_smul_distribView on Github →
2024-02-05 18:00
Mathlib/Data/Finset/Pointwise.lean
refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …
Modified Finset.image_smul_distribView on Github →
2023-03-27 18:03
Mathlib/Data/Finset/Pointwise.lean
feat: `s ∩ t * s ∪ t ⊆ s * t` (#1619) …
Added Finset.image_smul_distribView on Github →