English
Let T,S be rings with S a domain and an algebra T→S. If haroots : (C a X^2 + C b X + C c).aroots S = {x1,x2}, then algebraMap_T_S(c) = algebraMap_T_S(a) x1 x2.
Русский
Пусть T,S — кольца, S — область целостности, и есть алгебраическая карта T→S. Если haroots: (C a X^2 + C b X + C c).aroots S = {x1,x2}, тогда algebraMap_T_S(c) = algebraMap_T_S(a) x1 x2.
LaTeX
$$$$\\text{If }(C a X^2 + C b X + C c).aroots S = \\{x_1,x_2\\},\\; \\mathrm{algebraMap}_{T\\to S}(c) = \\mathrm{algebraMap}_{T\\to S}(a)\\,x_1 x_2. $$$$
Lean4
/-- **Vieta's formula** for quadratics (`aroots` version). -/
theorem eq_mul_mul_of_aroots_quadratic_eq_pair [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {a b c : T}
{x1 x2 : S} (haroots : (C a * X ^ 2 + C b * X + C c).aroots S = { x1, x2 }) :
algebraMap T S c = algebraMap T S a * x1 * x2 :=
by
rw [aroots_def,
show
map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) =
C ((algebraMap T S) a) * X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c)
by simp] at haroots
exact eq_mul_mul_of_roots_quadratic_eq_pair haroots
