c_of_eq

Mathlib.Algebra.CubicDiscriminant

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

English

If P.toPoly = Q.toPoly, then P.c = Q.c.

Русский

Если P.toPoly = Q.toPoly, то P.c = Q.c.

LaTeX

$$$ P.toPoly = Q.toPoly \\Rightarrow P.c = Q.c $$$

Lean4

theorem c_of_eq (h : P.toPoly = Q.toPoly) : P.c = Q.c := by rw [← coeff_eq_c, h, coeff_eq_c]

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

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

Разделы

Аффилиация

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