case h.e'_2.a
R : Type u
I : Type v
inst✝³ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on s) ↔ Pairwise (IsCoprime on fun i => s ↑i)
R : Type u
I : Type v
inst✝³ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ (∃ μ, ∑ i : I, μ i * ∏ j in {i}ᶜ, s j = 1) ↔ Pairwise (IsCoprime on s)
convert exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s) using 1
no goals
case h.e'_2.a
R : Type u
I : Type v
inst✝³ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on s) ↔ Pairwise (IsCoprime on fun i => s ↑i)
simp only [Function.onFun, pairwise_subtype_iff_pairwise_finset', coe_univ, Set.pairwise_univ]