Commit 2024-11-02 05:55 df174a8a

View on Github →

feat(Algebra/Group/Pointwise/Set): more gcongr lemmas (#17653) Tagging the two-arguments versions doesn't make gcongr fire on one-sided goals, so we also tag the one-sided versions. From PFR

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

modified theorem Set.smul_subset_smul_left

modified theorem Set.smul_subset_smul_right

modified theorem Set.vsub_subset_vsub

modified theorem Set.vsub_subset_vsub_left

modified theorem Set.vsub_subset_vsub_right