theorem Ideal.prod_span' {ι : Type u_1} {A : Type u_2} [CommSemiring A] (f : ι → A) (s : Finset ι) : Ideal.span {∏ i ∈ s, f i} = ∏ i ∈ s, Ideal.span {f i}

theorem Ideal.prod_map {ι : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring A] [CommSemiring B] [FunLike F A B] [RingHomClass F A B] (f : ι → Ideal A) (s : Finset ι) (χ : F) : Ideal.map χ (∏ i ∈ s, f i) = ∏ i ∈ s, Ideal.map χ (f i)