English
For any ideals I and a family J_i, the product distributes over the infimum: I * (⋂_i J_i) = ⋂_i (I * J_i).
Русский
Для идеала I и семейства J_i выполняется распределение произведения над инфимумом: I · (⋂_i J_i) = ⋂_i (I · J_i).
LaTeX
$$I * ⨅ i, J i = ⨅ i, I * J i$$
Lean4
theorem mul_iInf (I : Ideal A) {ι : Type*} [Nonempty ι] (J : ι → Ideal A) : I * ⨅ i, J i = ⨅ i, I * J i :=
by
by_cases hI : I = 0
· simp [hI]
refine (le_iInf fun i ↦ Ideal.mul_mono_right (iInf_le _ _)).antisymm ?_
have H : ⨅ i, I * J i ≤ I := (iInf_le _ (Nonempty.some ‹_›)).trans Ideal.mul_le_right
obtain ⟨K, hK⟩ := Ideal.dvd_iff_le.mpr H
rw [hK]
refine mul_le_mul_left' ?_ I
rw [le_iInf_iff]
intro i
rw [← mul_le_mul_iff_of_pos_left (a := I), ← hK]
· exact iInf_le _ _
· exact bot_lt_iff_ne_bot.mpr hI
