Commit 2025-07-16 01:19 488d3b8e

View on Github →

chore: fix four Submonoid recursors (#27185) Split from #27159.

Estimated changes

Modified Mathlib/Algebra/Group/Submonoid/Membership.lean

modified theorem Submonoid.closure_induction_left

modified theorem Submonoid.closure_induction_right

modified theorem Submonoid.induction_of_closure_eq_top_left

modified theorem Submonoid.induction_of_closure_eq_top_right

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean