Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.is_trichotomous_lex

Modification history

2022-06-04 19:44

src/data/pi/lex.lean

chore(data/pi/lex): turn `pi.lex.linear_order` into an instance (#14389) …

Added pi.is_trichotomous_lex View on Github →