coeff_eq_b

Mathlib.Algebra.CubicDiscriminant

URI: https://scilib.ai/kg/mathlib#Cubic.coeff_eq_b

English

The coefficient of X^2 in P.toPoly equals the coefficient b of the cubic P with a leading coefficient factored into the polynomial.

Русский

Коэффициент при X^2 в P.toPoly равен b кубика P.

LaTeX

$$$ (P.toPoly).coeff 2 = P.b $$$

Lean4

@[simp]
theorem coeff_eq_b : P.toPoly.coeff 2 = P.b :=
  coeffs.2.2.1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru