mathlib3

8cebd2b1 - chore(algebra/algebra): Split subalgebras into their own file (#4471)

chore(algebra/algebra): Split subalgebras into their own file (#4471) This matches how `subring` and `submonoid` both have their own files. This also remove `noncomputable theory` which is unnecessary for almost all the definitions