Theorem Nat.coprime_fintype_prod_left_iff

Modification history

2023-12-14 12:44
Mathlib/Data/Nat/GCD/BigOperators.lean
feat(Data/Nat/GCD/BigOperators): add lemmas about coprimality with `List.prod`, `Multiset.prod`, `Finset.prod` (#9005) …
Added Nat.coprime_fintype_prod_left_iffView on Github →