case h
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
⊢ x ∈ ↑Subalgebra.toSubmodule ⊥ ↔ x ∈ Submodule.span R {1}
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ↑Subalgebra.toSubmodule ⊥ = Submodule.span R {1}
ext x
no goals
case h
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
⊢ x ∈ ↑Subalgebra.toSubmodule ⊥ ↔ x ∈ Submodule.span R {1}
simp [mem_bot, Submodule.mem_span_singleton, Algebra.smul_def]