Topological (sub)algebras #
A topological algebra over a topological semiring
R is a topological semiring with a compatible
continuous scalar multiplication by elements of
R. We reuse typeclass
This is just a minimal stub for now!
The topological closure of a subalgebra is still a subalgebra, which as an algebra is a topological algebra.
If a subalgebra of a topological algebra is commutative, then so is its topological closure.
This is really a statement about topological algebra isomorphisms, but we don't have those, so we use the clunky approach of talking about an algebra homomorphism, and a separate homeomorphism, along with a witness that as functions they are the same.
If a subalgebra of a topological algebra is commutative, then so is its topological closure. See note [reducible non-instances].