Commit 2023-02-23 03:04 712146a5

View on Github →

feat: port GroupTheory.NoncommPiCoprod (#2449)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/NoncommPiCoprod.lean

added theorem MonoidHom.independent_range_of_coprime_order

added theorem MonoidHom.injective_noncommPiCoprod_of_independent

added def MonoidHom.noncommPiCoprod

added def MonoidHom.noncommPiCoprodEquiv

added theorem MonoidHom.noncommPiCoprod_mrange

added theorem MonoidHom.noncommPiCoprod_mulSingle

added theorem MonoidHom.noncommPiCoprod_range

added theorem Subgroup.commute_subtype_of_commute

added theorem Subgroup.eq_one_of_noncommProd_eq_one_of_independent

added theorem Subgroup.independent_of_coprime_order

added theorem Subgroup.injective_noncommPiCoprod_of_independent

added def Subgroup.noncommPiCoprod

added theorem Subgroup.noncommPiCoprod_mulSingle

added theorem Subgroup.noncommPiCoprod_range