Commit 2026-03-21 05:31 cf615727

View on Github →

chore: deprecate ConditionallyCompleteLinearOrderedField (#35760) Use the new mixin typeclass instead. Also, move the API for conditionally complete linear ordered fields into the ConditionallyCompleteLinearOrderedField namespace, and make instances scoped to this namespace. We should usually use instead.

Estimated changes

deleted theorem ringHom_monotone