Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.noncomm_pi_coprod_mul_single

Modification history

2022-03-16 11:53

src/group_theory/noncomm_pi_coprod.lean

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

Added subgroup.noncomm_pi_coprod_mul_single View on Github →