aroots_X — Mathlib

English

Let S be a domain and T → S an algebra. Then the roots of the polynomial X over S are exactly 0, i.e., X has a single root at 0 with multiplicity 1.

Русский

Пусть S — область, существует алгебраическое отображение T → S. Тогда корни полинома X в S равны {0}.

LaTeX

$$$$ \operatorname{aroots}(X)_S = \{0\} $$$$

Lean4

@[simp]
theorem aroots_X [CommRing S] [IsDomain S] [Algebra T S] : aroots (X : T[X]) S = {0} := by
  rw [aroots_def, map_X, roots_X]

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