Commit 2022-07-07 05:04 bf735cd1
View on Github →chore(set_theory/ordinal/basic): remove rel_iso_out (#15145)
This is just a specific application of rel_iso.cast. Moreover, it's unused.
chore(set_theory/ordinal/basic): remove rel_iso_out (#15145)
This is just a specific application of rel_iso.cast. Moreover, it's unused.