Skip to content

Commit

Permalink
doc(data/polynomial/basic): fix docstring (#15814)
Browse files Browse the repository at this point in the history
  • Loading branch information
negiizhao committed Aug 3, 2022
1 parent 777082d commit adc4ebc
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/data/polynomial/basic.lean
Expand Up @@ -32,7 +32,7 @@ the polynomials. For instance,
Polynomials are defined using `add_monoid_algebra R ℕ`, where `R` is a semiring.
The variable `X` commutes with every polynomial `p`: lemma `X_mul` proves the identity
`X * p = `p * X`. The relationship to `add_monoid_algebra R ℕ` is through a structure
`X * p = p * X`. The relationship to `add_monoid_algebra R ℕ` is through a structure
to make polynomials irreducible from the point of view of the kernel. Most operations
are irreducible since Lean can not compute anyway with `add_monoid_algebra`. There are two
exceptions that we make semireducible:
Expand Down

0 comments on commit adc4ebc

Please sign in to comment.