English
Let T,S be rings with a domain S and an algebra T→S. If (C a X^2 + C b X + C c).aroots S = {x1,x2}, then algebraMap_T_S(b) = - algebraMap_T_S(a) (x1 + x2).
Русский
Пусть T,S — кольца, S — интегральная область, и есть алгебраическая карта T→S. Если корни в S удовлетворяют (C a X^2 + C b X + C c).aroots S = {x1,x2}, то algebraMap_T_S(b) = - algebraMap_T_S(a) (x1 + x2).
LaTeX
$$$$\\text{If } (C a X^2 + C b X + C c).\\aroots S = \\{x_1,x_2\\}, \\text{ then } \\mathrm{algebraMap}_{T\\to S}(b) = -\\mathrm{algebraMap}_{T\\to S}(a)\,(x_1+x_2). $$$$
Lean4
/-- **Vieta's formula** for quadratics (`aroots` version). -/
theorem eq_neg_mul_add_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 b = -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_neg_mul_add_of_roots_quadratic_eq_pair haroots
