b_of_eq

Mathlib.Algebra.CubicDiscriminant

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

English

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

Русский

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

LaTeX

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

Lean4

theorem b_of_eq (h : P.toPoly = Q.toPoly) : P.b = Q.b := by rw [← coeff_eq_b, h, coeff_eq_b]

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

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

Разделы

Аффилиация

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