mathlib
bf735cd1
- chore(set_theory/ordinal/basic): remove `rel_iso_out` (#15145)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(set_theory/ordinal/basic): remove `rel_iso_out` (#15145) This is just a specific application of `rel_iso.cast`. Moreover, it's unused.
Author
vihdzp
Parents
9b2755b9
Loading