Commit 2024-08-02 07:08 6d1096a1

View on Github →

chore: backports for leanprover/lean4#4814 (part 13) (#15397) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

modified theorem Finset.sum_pow
modified theorem Finset.sum_pow_of_commute
modified theorem abelianizationCongr_of
modified theorem abelianizationCongr_symm
modified theorem abelianizationCongr_trans
modified theorem Subgroup.orderOf_le_card
modified theorem Submonoid.orderOf_le_card
modified theorem pow_mod_natCard
modified theorem zpow_mod_natCard
modified theorem PresentedGroup.toGroup.of
modified theorem SetTheory.PGame.Numeric.mul
modified theorem SetTheory.PGame.P24
modified theorem Set.Finite.isClopen_biInter
modified theorem Set.Finite.isClopen_biUnion
modified theorem isClopen_biInter_finset
modified theorem isClopen_biUnion_finset
modified theorem isClopen_iInter_of_finite
modified theorem isClopen_iUnion_of_finite