Commit 2025-07-29 19:02 86f7c47c

View on Github →

chore: generalize Subgroup.mem_mk and related lemmas (#27629)

Estimated changes

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

modified theorem Subgroup.coe_set_mk

modified theorem Subgroup.mem_mk

modified theorem Subgroup.mk_le_mk

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

Modified Mathlib/Analysis/Normed/Group/AddCircle.lean

Modified Mathlib/Combinatorics/Additive/VerySmallDoubling.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Defs.lean

Modified Mathlib/Topology/Algebra/Valued/ValuationTopology.lean