aroots_X_sub_C — Mathlib

English

Let S be a domain and T a ring with an algebra structure into S. For any r in T, the roots in S of the polynomial X − C(r) are exactly the image of r in S.

Русский

Пусть S — область, T — кольцо с алгебраической структурой над S. Для любого r ∈ T корни в S многочлена X − C(r) есть ровно образ r в S.

LaTeX

$$$$ \operatorname{aroots}(X - C(r))_S = \{\operatorname{algebraMap}_{T \to S}(r)\} $$$$

Lean4

@[simp]
theorem aroots_X_sub_C [CommRing S] [IsDomain S] [Algebra T S] (r : T) : aroots (X - C r) S = {algebraMap T S r} := by
  rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]

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