Commit 2025-03-13 06:05 ddfc8294

View on Github →

chore(*): fix some to_additive-generated names (#22836) Other changes:

Subgroup.bot_prod_bot is now @[simp]
IsMulFreimanHom.prod -> IsMulFreimanHom.prodMap
IsMulFreimanIso.prod -> IsMulFreimanIso.prodMap

Estimated changes

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

Modified Mathlib/Algebra/Group/Graph.lean

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

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

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

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

deleted theorem IsMulFreimanHom.prod

added theorem IsMulFreimanHom.prodMap

deleted theorem IsMulFreimanIso.prod

added theorem IsMulFreimanIso.prodMap

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

Modified Mathlib/GroupTheory/Coprod/Basic.lean

Modified Mathlib/GroupTheory/Coset/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/Index.lean

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

Modified Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean

Modified Mathlib/Topology/Algebra/UniformGroup/Defs.lean

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean