Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-14 12:19
09ea7fb0
View on Github →
feat(data/finset/noncomm_prod): finite pi lemmas (
#12291
) including a few helpers
Estimated changes
Modified
src/algebra/group/pi.lean
added
theorem
pi.mul_single_apply_commute
added
theorem
pi.mul_single_commute
Modified
src/data/finset/noncomm_prod.lean
added
theorem
finset.noncomm_prod_eq_pow_card
added
theorem
finset.noncomm_prod_map
added
theorem
finset.noncomm_prod_mul_single
added
theorem
monoid_hom.pi_ext
added
theorem
multiset.nocomm_prod_map_aux
added
theorem
multiset.noncomm_prod_eq_pow_card
added
theorem
multiset.noncomm_prod_map