coeff_eq_d

Mathlib.Algebra.CubicDiscriminant

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

English

The constant term of P.toPoly equals the coefficient d of the cubic P.

Русский

Постоянный член P.toPoly равен d кубического P.

LaTeX

$$$ (P.toPoly).coeff 0 = P.d $$$

Lean4

@[simp]
theorem coeff_eq_d : P.toPoly.coeff 0 = P.d :=
  coeffs.2.2.2.2

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

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

Разделы

Аффилиация

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