∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {s : I → R} [inst_1 : Fintype I] [Nonempty I]
  [inst_3 : DecidableEq I], (∃ μ, ∑ i, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (Function.onFun IsCoprime s)