F : Type ?u.698810
R : Type u_2
A : Type u_1
B : Type ?u.698819
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
⊢ Algebra.adjoin R (∅ ∪ star ∅) = Algebra.adjoin R ∅
F : Type ?u.698810
R : Type u_2
A : Type u_1
B : Type ?u.698819
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
⊢ ⊥.toSubalgebra = ⊥
change Algebra.adjoin R (∅ ∪ star ∅) = Algebra.adjoin R ∅
no goals
F : Type ?u.698810
R : Type u_2
A : Type u_1
B : Type ?u.698819
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
⊢ Algebra.adjoin R (∅ ∪ star ∅) = Algebra.adjoin R ∅
simp