rootSet_C_mul_X_pow — Mathlib

English

Let S be a commutative ring with no zero divisors and an R-algebra into S. If n ≠ 0 and a ≠ 0, then the polynomial C(a) · X^n has 0 as its only root in S.

Русский

Пусть S — коммутативное кольцо без делителей нуля и является алгеброй над R. При n ≠ 0 и a ≠ 0 корень полинома C(a) · X^n в S равен единственному корню 0.

LaTeX

$$$ n \neq 0 \land a \neq 0 \Rightarrow \operatorname{rootSet}(C a \cdot X^n) S = \{0\} $$$

Lean4

theorem rootSet_C_mul_X_pow [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) :
    rootSet (C a * X ^ n) S = {0} := by rw [C_mul_X_pow_eq_monomial, rootSet_monomial hn ha]

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