mathlib

717b11ec - feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups (#11744)

feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups (#11744) Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxumath@gmail.com>