mathlib3

658a3d77 - refactor(algebra/algebra): remove subalgebra.under (#10081)

refactor(algebra/algebra): remove subalgebra.under (#10081) This removes `subalgebra.under`, and replaces `subalgebra.of_under` with `subalgebra.of_restrict_scalars`. Lemmas associated with `under` have been renamed accordingly.