mathlib3
acc7dfa5
- chore(set_theory/surreal/basic): golf an instance (#15838)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(set_theory/surreal/basic): golf an instance (#15838) `subtype.setoid` is defeq to this manually specified instance.
Author
eric-wieser
Parents
c5e83e00
Loading