Commit 2024-02-08 19:09 28dae78b

View on Github →

feat: change Subgroup and Submonoid induction principles to work with induction (#9861) Induction principles have to be fully dependent in order to work with the induction tactic. This is usually a good thing anyway, since the dependent version is often more convenient to use, and avoids the caller having to fumble with generalizing over an existential. This changes the following induction principles (and their additive versions):

Submonoid.closure_induction_{left,right}
Subgroup.closure_induction_{left,right}
Subgroup.closure_induction'' (no submonoid version exists) Arguments to these lemmas have also been renamed to drop the H, as seems to be preferred for induction lemmas.

Estimated changes

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

modified theorem Subgroup.closure_induction''

modified theorem Subgroup.closure_induction_left

modified theorem Subgroup.closure_induction_right

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

modified theorem Submonoid.closure_induction_left

modified theorem Submonoid.closure_induction_right