Bundled order_embedding from algebraic substructures

Stream: general

[Junyan Xu]

In #17401 I made algebra.to_submodule an order_embedding, and I think the same could be done for all forgetful maps between lattices of algebraic substructures and for set_like.coe, which would save some boilerplate. Would be wonderful if someone does it systematically. There are some such maps that come from extends (e.g. docs#subalgebra.to_subsemiring) which aren't bundled by default though, so a new name would need to be assigned to the bundled version.

[Junyan Xu]

@Yaël Dillies I think you might be interested in this.

[Yaël Dillies]

We should be able to provide that for all function.injective.something_ordered, right?