Commit 2024-09-28 20:52 9b9053ea

View on Github →

feat(Pointwise): gcongr attributes and a few more lemmas (#17233) Also mark more lemmas as gcongr From LeanCamCombi

Estimated changes

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

added theorem Finset.inv_subset_div_right

added theorem Finset.smul_finset_insert

added theorem Finset.subset_div_left

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

added theorem Set.inv_subset_div_right

added theorem Set.smul_set_insert

modified theorem Set.smul_set_mono

added theorem Set.subset_div_left

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean