Skip to content

Commit

Permalink
docs(data/polynomial/algebra_map): fix a typo in a doc-string (#13989)
Browse files Browse the repository at this point in the history
The doc-string talks about `comm_ring`, while the lemma uses `comm_semiring`.  I aligned the two to the weaker one!
  • Loading branch information
adomani committed May 6, 2022
1 parent f6c030f commit fe0c4cd
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/data/polynomial/algebra_map.lean
Expand Up @@ -54,7 +54,7 @@ lemma of_finsupp_algebra_map (r : R) :
to_finsupp_injective (to_finsupp_algebra_map _).symm

/--
When we have `[comm_ring R]`, the function `C` is the same as `algebra_map R R[X]`.
When we have `[comm_semiring R]`, the function `C` is the same as `algebra_map R R[X]`.
(But note that `C` is defined when `R` is not necessarily commutative, in which case
`algebra_map` is not available.)
Expand Down

0 comments on commit fe0c4cd

Please sign in to comment.