Commit 2024-11-04 02:26 fef6aa3e

View on Github →

feat: add dsimp lemma for SetLike (#18453) The analogous lemma for Set already exists

Estimated changes

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

modified theorem Subgroup.singleton_mul_subgroup

modified theorem Subgroup.subgroup_mul_singleton

Modified Mathlib/Data/SetLike/Basic.lean

added theorem SetLike.setOf_mem_eq