Def RelEmbedding.Simps.apply

Modification history

2023-12-21 15:05
Mathlib/Order/RelIso/Basic.lean
feat(Order/RelIso): define missing instances (#9170) …
Deleted RelEmbedding.Simps.applyView on Github →
2022-11-30 20:20
Mathlib/Order/RelIso/Basic.lean
feat: port Order.RelIso.Basic (#772) …
Added RelEmbedding.Simps.applyView on Github →