Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.comap_injective_is_commutative

Modification history

2023-01-13 10:23
src/group_theory/subgroup/basic.lean
feat(group_theory/subgroup/basic): Map a subgroup under an iso (#17775) …
Modified subgroup.comap_injective_is_commutativeView on Github →
2022-08-23 10:32
src/group_theory/subgroup/basic.lean
feat(group_theory/subgroup/basic): Add `map_is_commutative` and `comap_injective_is_commutative` (#16109) …
Added subgroup.comap_injective_is_commutativeView on Github →