mathlib3

23270e71 - feat(ring_theory/adjoin): adjoining elements to form subalgebras (#756)

feat(ring_theory/adjoin): adjoining elements to form subalgebras (#756) * feat(ring_theory/adjoin): adjoining elements to form subalgebras * Fix build * Change to_submodule into a coercion * Use pointwise_mul * add simp attribute to adjoin_empty