aroots_C_mul_X_pow — Mathlib

English

If a ≠ 0, then the roots of C(a)·X^n are 0 with multiplicity n.

Русский

Если a ≠ 0, то корни C(a)·X^n — это 0 с кратностью n.

LaTeX

$$$$ (C(a)\cdot X^n)\aroots_S = n \cdot \{0\} \quad (a \neq 0) $$$$

Lean4

theorem aroots_C_mul_X_pow [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0)
    (n : ℕ) : (C a * X ^ n : T[X]).aroots S = n • ({0} : Multiset S) := by rw [aroots_C_mul _ ha, aroots_X_pow]

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