Theorems · Inductive type · field theory
Polynomial
(R : Type u_1) → [Semiring R] → Type u_1
Polynomial R is the type of univariate polynomials over R,
denoted as R[X] within the Polynomial namespace.
Polynomials should be seen as (semi-)rings with the additional constructor X.
The embedding from R is called C.
- Defined in
- Mathlib.Algebra.Polynomial.Basic
- Cited by
- 5,681 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
Cited by6,220
Results whose statement or proof uses this declaration.
- Polynomial.Xstatement · cited by 1,639
- Polynomial.Cstatement and proof · cited by 1,598
- Polynomial.natDegreestatement and proof · cited by 1,105
- Polynomial.coeffstatement and proof · cited by 1,045
- Polynomial.mapstatement · cited by 806
- Polynomial.evalstatement and proof · cited by 796
- Polynomial.degreestatement and proof · cited by 643
- Polynomial.aevalstatement · cited by 615
- Polynomial.leadingCoeffstatement and proof · cited by 498
- Polynomial.Monicstatement and proof · cited by 461
- minpolystatement and proof · cited by 439
- Polynomial.derivativestatement and proof · cited by 331
Showing the 200 most cited of 6,220.