no goals
α : Type u
β : Type v
inst✝² : Semiring α
I : Ideal α
a b : α
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
h : ⊥ = ⊤
⊢ 1 = 0
rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h
no goals
α : Type u
β : Type v
inst✝² : Semiring α
I : Ideal α
a b : α
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
x✝ y✝ : R
h : x✝ * y✝ ∈ ⊥
⊢ x✝ * y✝ = 0
simpa only [Submodule.mem_bot] using h