Commit 2021-03-04 21:18 744e79c1

View on Github →

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