Commit 2025-03-11 14:35 2496b17e

View on Github →

chore(*): fix some to_additive-generated names (#22818)

Estimated changes

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

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

Modified Mathlib/Geometry/Manifold/Algebra/Monoid.lean

Modified Mathlib/GroupTheory/Congruence/Defs.lean

Modified Mathlib/GroupTheory/Coset/Basic.lean

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean