Commit 2021-08-25 06:39 00e57d32
View on Github →chore(order/rel_iso): rename order_embedding.of_map_rel_iff to of_map_le_iff (#8839)
The old name comes from rel_embedding.
chore(order/rel_iso): rename order_embedding.of_map_rel_iff to of_map_le_iff (#8839)
The old name comes from rel_embedding.