Commit 2023-12-14 12:44 c6e2a243

View on Github →

feat(Data/Nat/GCD/BigOperators): add lemmas about coprimality with List.prod, Multiset.prod, Finset.prod (#9005) Add coprime_xxx_prod_left_iff, coprime_xxx_prod_right_iff lemma for List, Multiset, Finset and Fintype. This is a PR separated from #8887.

Estimated changes

Modified Mathlib/Data/Nat/GCD/BigOperators.lean

added theorem Nat.coprime_fintype_prod_left_iff

added theorem Nat.coprime_fintype_prod_right_iff

added theorem Nat.coprime_list_prod_left_iff

added theorem Nat.coprime_list_prod_right_iff

added theorem Nat.coprime_multiset_prod_left_iff

added theorem Nat.coprime_multiset_prod_right_iff

deleted theorem Nat.coprime_prod_left

added theorem Nat.coprime_prod_left_iff

deleted theorem Nat.coprime_prod_right

added theorem Nat.coprime_prod_right_iff

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean