Commit 2023-12-07 16:10 8289b55e

View on Github →

chore(Order/RelIso): drop a duplicate lemma (#2390) Duplicate of coe_fn_toEquiv several lines below.

Estimated changes

deleted theorem RelIso.coe_toEquiv