Theorem Set.image_op_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_op_smul_distribView on Github →
2025-01-05 13:11
Mathlib/Data/Set/Pointwise/SMul.lean
feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) …
Added Set.image_op_smul_distribView on Github →