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]