English
Pairwise coprimality of the family s_i indexed by t is equivalent to each s_i being coprime to the product of the rest.
Русский
Параллельно взаимная простота семейства s_i эквивалентна тому, что каждый s_i взаимно прост относительно произведения остальных.
LaTeX
$$$\text{Pairwise}(IsCoprime\ on\ fun\ i\to s_i) \iff \forall i\in t, IsCoprime\ (s_i)\left(\prod_{j\in t\setminus\{i\}} s_j\right)$$$
Lean4
theorem pairwise_coprime_iff_coprime_prod [DecidableEq I] :
Pairwise (IsCoprime on fun i : t ↦ s i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ { i }, s j) :=
by
rw [Finset.pairwise_subtype_iff_pairwise_finset']
refine ⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
· rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
exact (hp hj.1 hi hj.2).symm
· rintro i hi j hj h
apply IsCoprime.prod_right_iff.mp (hp i hi)
exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h (Finset.mem_singleton.mp f).symm⟩
