docs(ring_theory/adjoin_root): fix docstring (#9546)

leanprover-community · Oct 5, 2021 · 0491621 · 0491621
1 parent 7466424
commit 0491621
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ring_theory/adjoin_root.lean b/src/ring_theory/adjoin_root.lean
@@ -47,7 +47,7 @@ variables {R : Type u} {S : Type v} {K : Type w}
 open polynomial ideal
 
 /-- Adjoin a root of a polynomial `f` to a commutative ring `R`. We define the new ring
-as the quotient of `R` by the principal ideal of `f`. -/
+as the quotient of `polynomial R` by the principal ideal generated by `f`. -/
 def adjoin_root [comm_ring R] (f : polynomial R) : Type u :=
 ideal.quotient (span {f} : ideal (polynomial R))