mathlib3

5ff0dd42 - refactor(alebra/star/basic): weaken the meaning of `star_ordered_ring`

refactor(alebra/star/basic): weaken the meaning of `star_ordered_ring` This lets any commutative linearly ordered ring be considered a star ring with a trivial star operation.