Theorem Pi.toLex_apply

Modification history

2025-10-28 10:18

Mathlib/Order/PiLex.lean

feat: `CoeFun` for `Lex` and `Colex` (#30481) …

Modified Pi.toLex_apply View on Github →

2022-12-20 13:42

Mathlib/Data/Pi/Lex.lean

feat: port Data.Pi.Lex (#1104) …

Added Pi.toLex_apply View on Github →