roots_smul_nonzero

Mathlib.Algebra.Polynomial.Roots

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

English

If a is a unit, then the roots of C(a) X − C(b) are { a^{-1} b }.

Русский

Если a — единица, то корни C(a) X − C(b) равны { a^{-1} b }.

LaTeX

$$$ (C(a) \cdot X - C(b)).roots = \{ a^{-1} \cdot b \} $ for a ∈ R^×.$$

Lean4

@[simp]
theorem roots_smul_nonzero (p : R[X]) (ha : a ≠ 0) : (a • p).roots = p.roots := by rw [smul_eq_C_mul, roots_C_mul _ ha]

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

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

Разделы

Аффилиация

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