mathlib
19de4162
- doc(ring_theory/adjoin_root): add docstring (#2211)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
doc(ring_theory/adjoin_root): add docstring (#2211) * docstring for adjoin_root * adding some quotes
References
#2211 - doc(ring_theory/adjoin_root): add docstring
Author
kbuzzard
Parents
09401b7f
Loading