mathlib
06530557
- don't delete `ring_equiv_Cauchy`
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
don't delete `ring_equiv_Cauchy`
References
hrmacbeth-no-star-data-real-basic
Author
hrmacbeth
Parents
c8e53d55
Loading