resultant_C_right

Mathlib.RingTheory.Polynomial.Resultant.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.resultant_C_right

English

For polynomials f in R[X], natural m and a in R, the resultant of f with the constant C a equals a^m.

Русский

Для полиномов f в R[X], естественного m и элемента a ∈ R, резу́льтант f и C a равен a^m.

LaTeX

$$$\\operatorname{resultant} f (C a) m = a^{m}$$$

Lean4

/-- For polynomial `f` and constant `a`, `Res(f, a) = a ^ m`. -/
theorem resultant_C_right (a : R) : resultant f (C a) m = a ^ m := by simp

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

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

Разделы

Аффилиация

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