Commit 2022-01-14 08:37 fb2b1a01

fix(algebra/star/basic): redefine star_ordered_ring (#11213) This PR redefines star_ordered_ring to remove the ordered_semiring assumption, which includes undesirable axioms such as ∀ (a b c : α), a < b → 0 < c → c * a < c * b. See the discussion on Zulip here.