mathlib3

34853a95 - feat(topology/algebra/algebra): define the topological subalgebra generated by an element (#13093)

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!