mathlib
d6b4cd7b
- chore(ring_theory/adjoin/basic): split (#9257)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(ring_theory/adjoin/basic): split (#9257) I want to use basic facts about `adjoin` in `polynomial.basic`.
Author
urkud
Parents
0ee36a39
Loading