Def LinearExtension

Modification history

2023-01-03 18:09
Mathlib/Order/Extension/Linear.lean
feat port: Order.Extension.Linear (#1309) …
Added LinearExtensionView on Github →