toPoly — Mathlib

English

Given a cubic with coefficients a,b,c,d in a semiring R, the associated polynomial is a X^3 + b X^2 + c X + d.

Русский

Дано кубическое с коэффициентами a,b,c,d в полупорядоченном кольце R; соответствующий полином равен a X^3 + b X^2 + c X + d.

LaTeX

$$$ \\text{toPoly}(P) = C(P.a) X^3 + C(P.b) X^2 + C(P.c) X + C(P.d) $$$

Lean4

/-- Convert a cubic polynomial to a polynomial. -/
def toPoly (P : Cubic R) : R[X] :=
  C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d

Похожие утверждения