Theorem Set.smul_set_mono
Modification history
2025-08-02 07:11
Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean
chore: deprecate `Set.image_subset` (#27287) …
Modified Set.smul_set_monoView on Github →2025-03-30 23:38
Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
chore(Algebra/Group/Pointwise/{Fin}set/Basic): split files (#23429) …
Modified Set.smul_set_monoView on Github →2024-09-28 20:52
Mathlib/Algebra/Group/Pointwise/Set.lean
feat(Pointwise): `gcongr` attributes and a few more lemmas (#17233) …
Modified Set.smul_set_monoView on Github →