α : Type u
β : Type v
inst✝ : Semiring α
a b : α
⊢ 1 ∈ ⊤
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
⊢ I = ⊤ → 1 ∈ I
rintro rfl
no goals
α : Type u
β : Type v
inst✝ : Semiring α
a b : α
⊢ 1 ∈ ⊤
trivial
no goals
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
h : 1 ∈ I
⊢ 1 * 1 = 1
simp