mathlib

a7563333 - chore(algebra/algebra/subalgebra): Add missing coe_sort for subalgebra (#6800)

chore(algebra/algebra/subalgebra): Add missing coe_sort for subalgebra (#6800) Unlike all the other subobject types, `subalgebra` does not implement `has_coe_to_sort` directly, instead going via a coercion to one of `submodule` and `subsemiring`. This removes the `has_coe (subalgebra R A) (subsemiring A)` and `has_coe (subalgebra R A) (submodule R A)` instances; we don't have these for any other subobjects, and they cause the elaborator more difficulty than the corresponding `to_subsemiring` and `to_submodule` projections. This changes the definition of `le` to not involve coercions, which matches `submodule` but requires a few proofs to change. This speeds up the `lift_of_splits` proof by adding `finite_dimensional.of_subalgebra_to_submodule`.