Structure ConditionallyCompleteLinearOrderedField

Modification history

2026-08-31 13:50
Mathlib/Algebra/Order/CompleteField.lean
chore: delete deprecated declarations from February 2026 (#43178) …
Deleted ConditionallyCompleteLinearOrderedFieldView on Github →
2026-03-21 05:31
Mathlib/Algebra/Order/CompleteField.lean
chore: deprecate `ConditionallyCompleteLinearOrderedField` (#35760) …
Added ConditionallyCompleteLinearOrderedFieldView on Github →