Commit 2022-08-23 10:32 62ac221e

View on Github →

feat(group_theory/subgroup/basic): Add map_is_commutative and comap_injective_is_commutative (#16109) This PR adds map_is_commutative and comap_injective_is_commutative.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.comap_injective_is_commutative