α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h : ⊥ = ⊤
⊢ ¬1 ∈ ⊥
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h : ⊥ = ⊤
⊢ ¬1 ∈ ⊤
rw [← h]
no goals
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h : ⊥ = ⊤
⊢ ¬1 ∈ ⊥
simp