Theorem ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff

Modification history

2026-03-21 05:31
Mathlib/Algebra/Order/CompleteField.lean
chore: deprecate `ConditionallyCompleteLinearOrderedField` (#35760) …
Added ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iffView on Github →