conj): `conj_classes.map` preserves surjectivity (#11362)

Commit

3 years ago

feat(algebra/group/conj): `conj_classes.map` preserves surjectivity (#11362) If `f : α →* β` is surjective, then so is `conj_classes.map f : conj_classes α → conj_classes β`.

Author

tb65536

Parents

c94a17c7

mathlib3 02181c76 - feat(algebra/group/conj): `conj_classes.map` preserves surjectivity (#11362)

mathlib3
02181c76 - feat(algebra/group/conj): `conj_classes.map` preserves surjectivity (#11362)