Theorem RelEmbedding.inj

Modification history

2023-12-21 15:05

Mathlib/Order/RelIso/Basic.lean

feat(Order/RelIso): define missing instances (#9170) …

Modified RelEmbedding.inj View on Github →

2023-11-08 21:29

Mathlib/Order/RelIso/Basic.lean

chore(Order): restore missing simp attribute (#8162) …

Modified RelEmbedding.inj View on Github →

2022-11-30 20:20

Mathlib/Order/RelIso/Basic.lean

feat: port Order.RelIso.Basic (#772) …

Added RelEmbedding.inj View on Github →