R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset ι
f : ι → Ideal R
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
⊢ (∃ I, I ∈ Multiset.map f s ∧ I ≤ P) ↔ ∃ i, i ∈ s ∧ f i ≤ P
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset ι
f : ι → Ideal R
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
⊢ Multiset.prod (Multiset.map f s) ≤ P ↔ ∃ i, i ∈ s ∧ f i ≤ P
rw [hp.multiset_prod_le (mt Multiset.map_eq_zero.mp hne)]
no goals
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset ι
f : ι → Ideal R
P : Ideal R
hp : IsPrime P
hne : s ≠ 0
⊢ (∃ I, I ∈ Multiset.map f s ∧ I ≤ P) ↔ ∃ i, i ∈ s ∧ f i ≤ P
simp_rw [Multiset.mem_map, exists_exists_and_eq_and]