Def toLinearExtension

Modification history

2025-05-02 23:00

Mathlib/Order/Extension/Linear.lean

chore: bump toolchain to v4.20.0-rc2 (#24561)

Deleted toLinearExtension View on Github →

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 →