aroots_smul_nonzero

Mathlib.Algebra.Polynomial.Roots

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

← MathLib Explorer

English

If a ≠ 0, then (a · p) has the same roots as p.

Русский

Если a ≠ 0, то (a · p) имеет те же корни, что и p.

LaTeX

$$$$ (a\cdot p)\aroots_S = p\aroots_S \quad (a \neq 0) $$$$

Lean4

@[simp]
theorem aroots_smul_nonzero [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (p : T[X])
    (ha : a ≠ 0) : (a • p).aroots S = p.aroots S := by rw [smul_eq_C_mul, aroots_C_mul _ ha]

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

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

Разделы

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

Аффилиация

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