English
If J maps to a finite family of ideals, and each is coprime with I, then I is coprime with their infimum over the family.
Русский
Если у I есть сопутствующая би-часть-Inf, и каждая пара (I, J_j) взаимно проста, то IsCoprime I (⋂_j J_j).
LaTeX
$$$$ IsCoprime I (\iota \to J\, ) $$$$
Lean4
theorem isCoprime_biInf {J : ι → Ideal R} {s : Finset ι} (hf : ∀ j ∈ s, IsCoprime I (J j)) :
IsCoprime I (⨅ j ∈ s, J j) := by
classical
simp_rw [isCoprime_iff_add] at *
induction s using Finset.induction with
| empty => simp
| insert i s _ hs =>
rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
set K := ⨅ j ∈ s, J j
calc
1 = I + K := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
_ = I + K * (I + J i) := by rw [hf i (Finset.mem_insert_self i s), mul_one]
_ = (1 + K) * I + K * J i := by ring
_ ≤ I + K ⊓ J i := add_le_add mul_le_left mul_le_inf
