Commit 2025-01-09 08:48 5e91013b

View on Github →

feat: pointwise set operations commute with cartesian product (#20579) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

added theorem Finset.inv_product

added theorem Finset.one_product_one

added theorem Finset.product_mul_product_comm

added theorem Finset.product_pow

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

added theorem Set.inv_prod

added theorem Set.one_prod_one

added theorem Set.prod_mul_prod_comm

added theorem Set.prod_pow

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean