c_eq_three_roots

Mathlib.Algebra.CubicDiscriminant

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

← MathLib Explorer

English

If a ≠ 0 and the mapped roots are x, y, z, then φ P.c = φ P.a (xy + xz + yz).

Русский

Если a ≠ 0 и корни map φ P равны x, y, z, то φ P.c = φ P.a (xy + xz + yz).

LaTeX

$$$$\\varphi P.c = \\varphi P.a (xy + xz + yz).$$$$

Lean4

theorem c_eq_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = { x, y, z }) :
    φ P.c = φ P.a * (x * y + x * z + y * z) := by injection eq_sum_three_roots ha h3

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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