Commit 2024-05-15 06:18 5cc7b947

feat: Algebra.adjoin R s is span R {1} ⊔ s.toSubmodule (#12889) This relates several unital and non-unital subobject closures to each other the to various counterparts. This is one of the key steps towards establishing that C(s, 𝕜)₀ is the closure of the non-unital star subalgebra generated by the identity function, when s is compact and RCLike 𝕜. This, in turn, is essential for writing instances of the continuous functional calculus for non-unital algebras.