Def toLinearExtension

Modification history

2023-12-23 07:20

Mathlib/Order/Extension/Linear.lean

refactor(Order/Extension): use `OrderHom` (#9232) …

Modified toLinearExtension View on Github →

2023-01-03 18:09

Mathlib/Order/Extension/Linear.lean

feat port: Order.Extension.Linear (#1309) …

Added toLinearExtension View on Github →