Commit 2024-04-24 13:42 49b417ef

View on Github →

feat(GroupTheory): add lemmas about Submonoid.closure and CoprodI (#12391)

Add CoprodI.lift_comp_of, CoprodI.lift_comp_of', CoprodI.lift_of', CoprodI.iSup_mrange_of, CoprodI.mclosure_iUnion_range_of, CoprodI.induction_left
Add MonoidHom.mrange_id, MonoidHom.mclosure_range, as well as additive versions.

Estimated changes

Modified Mathlib/GroupTheory/CoprodI.lean

added theorem Monoid.CoprodI.iSup_mrange_of

added theorem Monoid.CoprodI.induction_left

added theorem Monoid.CoprodI.lift_comp_of'

added theorem Monoid.CoprodI.lift_comp_of

modified theorem Monoid.CoprodI.lift_mrange_le

added theorem Monoid.CoprodI.lift_of'

modified theorem Monoid.CoprodI.lift_of

added theorem Monoid.CoprodI.mclosure_iUnion_range_of

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

added theorem MonoidHom.mclosure_range

added theorem MonoidHom.mrange_id