Theorem ConditionallyCompleteLinearOrderedField.inducedMap_nonneg

Modification history

2026-09-28 14:01
Mathlib/Algebra/Order/CompleteField.lean
chore: golf proofs with `grw`/`gcongr`/`gconvert` (#44245)
Modified ConditionallyCompleteLinearOrderedField.inducedMap_nonnegView on Github →
2026-03-21 05:31
Mathlib/Algebra/Order/CompleteField.lean
chore: deprecate `ConditionallyCompleteLinearOrderedField` (#35760) …
Added ConditionallyCompleteLinearOrderedField.inducedMap_nonnegView on Github →