mathlib3
198161d8 - feat(data/prod/basic): `prod.lex` is trichotomous (#17931)

Commit
3 years ago
feat(data/prod/basic): `prod.lex` is trichotomous (#17931) or irreflexive when the base relations are.
Author
Parents
Loading