Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-16 11:53 717b11ec

View on Github →

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

Estimated changes

Created src/group_theory/noncomm_pi_coprod.lean

added theorem monoid_hom.independent_range_of_coprime_order

added theorem monoid_hom.injective_noncomm_pi_coprod_of_independent

added def monoid_hom.noncomm_pi_coprod

added def monoid_hom.noncomm_pi_coprod_equiv

added theorem monoid_hom.noncomm_pi_coprod_mrange

added theorem monoid_hom.noncomm_pi_coprod_mul_single

added theorem monoid_hom.noncomm_pi_coprod_range

added theorem subgroup.commute_subtype_of_commute

added theorem subgroup.independent_of_coprime_order

added theorem subgroup.injective_noncomm_pi_coprod_of_independent

added def subgroup.noncomm_pi_coprod

added theorem subgroup.noncomm_pi_coprod_mul_single

added theorem subgroup.noncomm_pi_coprod_range

Modified src/group_theory/order_of_element.lean

added theorem order_of_inv

added theorem order_of_map_dvd

Modified src/group_theory/subgroup/basic.lean

modified theorem subgroup.eq_one_of_noncomm_prod_eq_one_of_independent