Commit 2025-08-29 18:14 af7b2e83

View on Github →

feat(Algebra/Group): add theorems about Submonoid.inclusion (#29035)

Estimated changes

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

modified theorem Subgroup.coe_inclusion

modified theorem SubgroupClass.coe_inclusion

modified theorem SubgroupClass.subtype_comp_inclusion

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

added theorem Submonoid.coe_inclusion

added theorem Submonoid.inclusion_inj

added theorem Submonoid.inclusion_injective

added theorem Submonoid.subtype_comp_inclusion