Theorem Set.image_smul_distrib

Modification history

2025-03-29 10:26
Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean
feat: generalize Mathlib.Algebra.Group+Ring+Field (#23143) …
Modified Set.image_smul_distribView on Github →
2025-03-03 17:20
Mathlib/Algebra/Group/Action/Pointwise/Set.lean
chore(Data/Set/Pointwise/SMul): move content to earlier files (#20793) …
Modified Set.image_smul_distribView on Github →
2024-02-05 18:00
Mathlib/Data/Set/Pointwise/SMul.lean
refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …
Modified Set.image_smul_distribView on Github →
2023-03-27 18:03
Mathlib/Data/Set/Pointwise/SMul.lean
feat: `s ∩ t * s ∪ t ⊆ s * t` (#1619) …
Added Set.image_smul_distribView on Github →