mathlib3

744e79c1 - feat(algebra/ordered_*, */sub{monoid,group,ring,semiring,field,algebra}): pullback of ordered algebraic structures under an injective map (#6489)

feat(algebra/ordered_*, */sub{monoid,group,ring,semiring,field,algebra}): pullback of ordered algebraic structures under an injective map (#6489) Prove that the following 14 order typeclasses can be pulled back via an injective map (`function.injective.*`), and use them to attach 30 new instances to sub-objects: * `ordered_comm_monoid` (and the implied `ordered_add_comm_monoid`) * `submonoid.to_ordered_comm_monoid` * `submodule.to_ordered_add_comm_monoid` * `ordered_comm_group` (and the implied `ordered_add_comm_group`) * `subgroup.to_ordered_comm_group` * `submodule.to_ordered_add_comm_group` * `ordered_cancel_comm_monoid` (and the implied `ordered_cancel_add_comm_monoid`) * `submonoid.to_ordered_cancel_comm_monoid` * `submodule.to_ordered_cancel_add_comm_monoid` * `linear_ordered_cancel_comm_monoid` (and the implied `linear_ordered_cancel_add_comm_monoid`) * `submonoid.to_linear_ordered_cancel_comm_monoid` * `submodule.to_linear_ordered_cancel_add_comm_monoid` * `linear_ordered_comm_monoid_with_zero` * (no suitable subobject exists for monoid_with_zero) * `linear_ordered_comm_group` (and the implied `linear_ordered_add_comm_group`) * `subgroup.to_linear_ordered_comm_group` * `submodule.to_linear_ordered_add_comm_group` * `ordered_semiring` * `subsemiring.to_ordered_semiring` * `subalgebra.to_ordered_semiring` * `ordered_comm_semiring` * `subsemiring.to_ordered_comm_semiring` * `subalgebra.to_ordered_comm_semiring` * `ordered_ring` * `subring.to_ordered_ring` * `subalgebra.to_ordered_ring` * `ordered_comm_ring` * `subring.to_ordered_comm_ring` * `subalgebra.to_ordered_comm_ring` * `linear_ordered_semiring` * `subring.to_linear_ordered_semiring` * `subalgebra.to_linear_ordered_semiring` * `linear_ordered_ring` * `subring.to_linear_ordered_ring` * `subalgebra.to_linear_ordered_ring` * `linear_ordered_comm_ring` * `subring.to_linear_ordered_comm_ring` * `subalgebra.to_linear_ordered_comm_ring` * `linear_ordered_field` * `subfield.to_linear_ordered_field` Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rings.20from.20subtype Co-authored-by: Eric Wieser <wieser.eric@gmail.com>