roots_C_mul

Mathlib.Algebra.Polynomial.Roots

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

← MathLib Explorer

English

If a ≠ 0 in R, then (C a) p has the same roots as p.

Русский

Если a ≠ 0, то корни C a · p совпадают с корнями p.

LaTeX

$$$ a \neq 0 \Rightarrow (C a \cdot p).roots = p.roots $$$

Lean4

@[simp]
theorem roots_C_mul (p : R[X]) (ha : a ≠ 0) : (C a * p).roots = p.roots := by
  by_cases hp : p = 0 <;>
    simp only [roots_mul, *, Ne, mul_eq_zero, C_eq_zero, or_self_iff, not_false_iff, roots_C, zero_add, mul_zero]

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

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

Разделы

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

Аффилиация

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