rootSet_X_pow — Mathlib

English

Let S be a commutative domain with an R-algebra structure into S. Then for every n ≠ 0, the polynomial X^n has root set {0} in S.

Русский

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

LaTeX

$$$ n \neq 0 \Rightarrow (X^n : R[X]).rootSet S = \{0\} $$$

Lean4

theorem rootSet_X_pow [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) : (X ^ n : R[X]).rootSet S = {0} :=
  by
  rw [← one_mul (X ^ n : R[X]), ← C_1, rootSet_C_mul_X_pow hn]
  exact one_ne_zero

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