Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-16 17:35 06886125

View on Github →

feat(order/rel_iso): constructors for rel embeddings (#7046) Alternate constructors for relation and order embeddings which require slightly less to prove.

Estimated changes