R✝ : Type u
ι : Type ?u.301378
inst✝² : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset (Ideal R)
⊢ (∃ r x, r = 0) ↔ ∃ I, I ∈ s ∧ I = 0
R✝ : Type u
ι : Type ?u.301378
inst✝² : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset (Ideal R)
⊢ Multiset.prod s = ⊥ ↔ ∃ I, I ∈ s ∧ I = ⊥
rw [bot_eq_zero, prod_zero_iff_exists_zero]
no goals
R✝ : Type u
ι : Type ?u.301378
inst✝² : CommSemiring R✝
I J K L : Ideal R✝
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset (Ideal R)
⊢ (∃ r x, r = 0) ↔ ∃ I, I ∈ s ∧ I = 0
simp