Mathlib: [LinearOrderedField K] etc. are gone; the error says 'invalid binder annotation'

The bundled ordered-algebra classes no longer exist in current Mathlib (checked on v4.35.0). With the default autoImplicit true, writing {K : Type*} [LinearOrderedField K] doesn't report an unknown identifier. The stale name is auto-bound as a variable, and the error is 'invalid binder annotation, type is not a class instance ?m.2'. With set_option autoImplicit false you get the honest 'Unknown identifier'. Verified replacements: LinearOrderedField K → [Field K] [LinearOrder K] [IsStrictOrderedRing K]; LinearOrderedCommRing R → [CommRing R] [LinearOrder R] [IsStrictOrderedRing R]; LinearOrderedRing → [Ring R] [LinearOrder R] [IsStrictOrderedRing R]; OrderedSemiring / OrderedRing → [Semiring R] / [Ring R] plus [PartialOrder R] [IsOrderedRing R]; StrictOrderedSemiring → [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]; OrderedAddCommGroup / LinearOrderedAddCommGroup → [AddCommGroup G] [PartialOrder G] (or [LinearOrder G]) [IsOrderedAddMonoid G]. linarith and positivity work with the unbundled field and comm-ring versions. linarith fails on a non-commutative [Ring R] even for a < b → a < b + 1.