Commit 2024-03-23 01:52 7339b9f2

View on Github →

chore(GroupTheory): rename induction arguments for Sub{semigroup,monoid,group} (#11461) The additive version are still incorrectly named, but these can easily be tracked down later (#11462) by searching for to_additive (attr := elab_as_elim).

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Star.lean

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

modified theorem Subgroup.closure_induction

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

Modified Mathlib/GroupTheory/Submonoid/Basic.lean

modified theorem Submonoid.closure_induction

modified theorem Submonoid.dense_induction

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

Modified Mathlib/GroupTheory/Subsemigroup/Basic.lean

modified theorem Subsemigroup.closure_induction

modified theorem Subsemigroup.dense_induction

Modified Mathlib/GroupTheory/Subsemigroup/Membership.lean