Commit 2022-04-12 08:46 34853a95

feat(topology/algebra/algebra): define the topological subalgebra generated by an element (#13093) This defines the topological subalgebra generated by a single element x : A of an algebra A as the topological closure of algebra.adjoin R {x}, and show it is commutative. I called it algebra.elemental_algebra; if someone knows if this actually has a name in the literature, or just has a better idea for the name, let me know!