Commit 2023-01-31 19:45 9c6f7958

View on Github →

feat: port Algebra.BigOperators.Associated (#1943)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Associated.lean

added theorem Associates.exists_mem_multiset_le_of_prime

added theorem Associates.finset_prod_mk

added theorem Associates.prod_eq_one_iff

added theorem Associates.prod_le_prod

added theorem Associates.prod_mk

added theorem Associates.rel_associated_iff_map_eq_map

added theorem Finset.prod_primes_dvd

added theorem Multiset.prod_ne_zero_of_prime

added theorem Multiset.prod_primes_dvd

added theorem Prime.dvd_finset_prod_iff

added theorem Prime.dvd_finsupp_prod_iff

added theorem Prime.exists_mem_finset_dvd

added theorem Prime.exists_mem_multiset_dvd

added theorem Prime.exists_mem_multiset_map_dvd

added theorem exists_associated_mem_of_dvd_prod