coeff_eq_a

Mathlib.Algebra.CubicDiscriminant

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

English

The coefficient of X^3 in P.toPoly equals the leading coefficient a of the cubic P.

Русский

Коэффициент при X^3 в P.toPoly равен a кубического P.

LaTeX

$$$ (P.toPoly).coeff 3 = P.a $$$

Lean4

@[simp]
theorem coeff_eq_a : P.toPoly.coeff 3 = P.a :=
  coeffs.2.1

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

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

Разделы

Аффилиация

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