Theorem Prod.Lex.toLex_strictMono

Modification history

2023-12-26 22:33
Mathlib/Data/Prod/Lex.lean
chore: remove workarounds for lean4#1891 (#9290) …
Modified Prod.Lex.toLex_strictMonoView on Github →
2022-11-29 20:45
Mathlib/Data/Prod/Lex.lean
feat(Data.Prod.Lex): port file (#783) …
Added Prod.Lex.toLex_strictMonoView on Github →