English
Let T,S be rings with ha : algebraMap T S a ≠ 0. Then (C a X^2 + C b X + C c).aroots S = { x1, x2 } iff algebraMap T S b = - algebraMap T S a (x1 + x2) and algebraMap T S c = algebraMap T S a x1 x2.
Русский
Пусть ha: алгебраическая карта T→S не нуль. Тогда (C a X^2 + C b X + C c).aroots S = { x1, x2 } тогда эквивалентно algebraMap_T_S(b) = - algebraMap_T_S(a)(x1+x2) и algebraMap_T_S(c) = algebraMap_T_S(a) x1 x2.
LaTeX
$$$$\\text{ha}:\\ algebraMap_{T\\to S}(a)\\neq 0 \\;\n\\Rightarrow\\; (C a X^2 + C b X + C c).aroots S = \\{x_1,x_2\\} \n\\iff\\; algebraMap_{T\\to S}(b) = - algebraMap_{T\\to S}(a) (x_1+x_2) \\\\text{and}\\; algebraMap_{T\\to S}(c) = algebraMap_{T\\to S}(a) x_1 x_2.$$$$
Lean4
/-- **Vieta's formula** for quadratics as an iff (`aroots` version). -/
theorem aroots_quadratic_eq_pair_iff_of_ne_zero [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {a b c : T}
{x1 x2 : S} (ha : algebraMap T S a ≠ 0) :
(C a * X ^ 2 + C b * X + C c).aroots S = { x1, x2 } ↔
algebraMap T S b = -algebraMap T S a * (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]
exact roots_quadratic_eq_pair_iff_of_ne_zero ha
