English
ForDecidableEq I, Pairwise IsRelPrime on the family s over I is equivalent to the condition that each s(i) is coprime to the product of the rest of the s(j) for j ≠ i.
Русский
Для DecidableEq I взаимная попарная простота семейства s над I эквивалентна тому, что каждый s(i) взаимно прост с произведением остальных s(j) для j ≠ i.
LaTeX
$$ [DecidableEq I] : Pairwise (IsRelPrime on fun i : t ↦ s i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ { i }, s j)$$
Lean4
theorem pairwise_isRelPrime_iff_isRelPrime_prod [DecidableEq I] :
Pairwise (IsRelPrime on fun i : t ↦ s i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ { i }, s j) :=
by
refine ⟨fun hp i hi ↦ IsRelPrime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
· rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
obtain ⟨hj, ji⟩ := hj
exact @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm
· rintro ⟨i, hi⟩ ⟨j, hj⟩ h
apply IsRelPrime.prod_right_iff.mp (hp i hi)
grind
