English
Let T,S be rings with 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 — кольца, haroots: ... тогда 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\\}, \\text{ then } algebraMap_{T\\to S}(c) = algebraMap_{T\\to S}(a)\\, x_1 x_2.$$$$
Lean4
/-- **Vieta's formula** for quadratics as an iff (`aroots, Field` version). -/
theorem aroots_quadratic_eq_pair_iff_of_ne_zero' [CommRing T] [Field 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 } ↔
x1 + x2 = -algebraMap T S b / algebraMap T S a ∧ x1 * x2 = algebraMap T S c / algebraMap T S a :=
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
