English
In a finite index set, there exists a linear combination of the s_i and products of the others equaling 1 if and only if the s_i are pairwise coprime.
Русский
Для конечного набора индексов существует линейная комбинация s_i и произведений остальных, равная единице, тогда и только тогда, когда элементы попарно взаимно просты.
LaTeX
$$$\exists \mu: I \to R, \left( \sum_{i\in t} \mu_i \prod_{j\in t \setminus \{i\}} s_j \right) = 1 \iff (t : Set I).Pairwise (IsCoprime on\ s)$$$
Lean4
theorem exists_sum_eq_one_iff_pairwise_coprime' [Fintype I] [Nonempty I] [DecidableEq I] :
(∃ μ : I → R, (∑ i : I, μ i * ∏ j ∈ { i }ᶜ, s j) = 1) ↔ Pairwise (IsCoprime on s) :=
by
convert exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s) using 1
simp only [pairwise_subtype_iff_pairwise_finset', coe_univ, Set.pairwise_univ]
