mathlib3

7d34f786 - chore(algebra/algebra/subalgebra): reduce imports (#12636)

chore(algebra/algebra/subalgebra): reduce imports (#12636) Splitting a file, and reducing imports. No change in contents. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>