Theorem extend_partial_order

Modification history

2023-01-07 14:35
Mathlib/Order/Extension/Linear.lean
chore: tidy various files (#1412)
Deleted extend_partial_orderView on Github →
2023-01-03 18:09
Mathlib/Order/Extension/Linear.lean
feat port: Order.Extension.Linear (#1309) …
Added extend_partial_orderView on Github →