star_ordered_ring.to_ordered_add_comm_group

Stream: general

[Yaël Dillies]

Isn't docs#star_ordered_ring.to_ordered_add_comm_group a very bad instance? It derives ordered_add_comm_group R from [non_unital_ring R] [partial_order R] [star_ordered_ring R], but partial_order R can be derived from ordered_add_comm_group R.

[Alex J. Best]

It's fine in lean 4 right?

[Jireh Loreaux]

It didn't give us issues in Lean 3, but star_ordered_ring was not used that much yet, so maybe it would have eventually. I think loops are fine in Lean 4 though.