Commit 2021-03-24 13:49 a7563333

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.