fix(data/polynomial/basic): op_ring_equiv docstring (#13132)

leanprover-community · Apr 3, 2022 · 61e18ae · 61e18ae
1 parent 36e1cdf
commit 61e18ae
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/data/polynomial/basic.lean b/src/data/polynomial/basic.lean
@@ -175,7 +175,8 @@ def to_finsupp_iso : R[X] ≃+* add_monoid_algebra R ℕ :=
   map_mul' := by { rintros ⟨⟩ ⟨⟩, simp [mul_to_finsupp] },
   map_add' := by { rintros ⟨⟩ ⟨⟩, simp [add_to_finsupp] } }
 
-/-- Ring isomorphism between `R[X]ᵐᵒᵖ` and `R[X]ᵐᵒᵖ`. -/
+/-- Ring isomorphism between `R[X]ᵐᵒᵖ` and `Rᵐᵒᵖ[X]` sending each coefficient of a polynomial
+to the corresponding element of the opposite ring. -/
 @[simps]
 def op_ring_equiv : R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X] :=
 ((to_finsupp_iso R).op.trans add_monoid_algebra.op_ring_equiv).trans (to_finsupp_iso _).symm