basic): Add `map_is_commutative` and `comap_injective_is_commutative` (#16109)

Commit

3 years ago

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`.

Author

tb65536

Parents

fadfe79b

mathlib 62ac221e - feat(group_theory/subgroup/basic): Add `map_is_commutative` and `comap_injective_is_commutative` (#16109)

mathlib
62ac221e - feat(group_theory/subgroup/basic): Add `map_is_commutative` and `comap_injective_is_commutative` (#16109)