English
Let T be a domain with a field S and an algebra T→S. Then (C a X^2 + C b X + C c).aroots S = { x1, x2 } iff x1 + x2 = - (algebraMap T S b) / (algebraMap T S a) and x1 x2 = (algebraMap T S c) / (algebraMap T S a).
Русский
Пусть T — домен, S — поле над T, и есть алгебраическая карта T→S. Тогда (C a X^2 + C b X + C c).aroots S = { x1, x2 } эквивалентно ...
LaTeX
$$$$\\text{If } ha:\\ algebraMap_{T\\to S}(a) \\neq 0, \\; (C a X^2 + C b X + C c).aroots S = \\{x_1,x_2\\} \iff x_1+x_2 = -\\frac{algebraMap_{T\\to S}(b)}{algebraMap_{T\\to S}(a)} \\wedge x_1 x_2 = \\frac{algebraMap_{T\\to S}(c)}{algebraMap_{T\\to S}(a)}.$$$$
Lean4
/-- **Vieta's formula** for quadratics as an iff (`Field` version). -/
theorem roots_quadratic_eq_pair_iff_of_ne_zero' [Field R] {a b c x1 x2 : R} (ha : a ≠ 0) :
(C a * X ^ 2 + C b * X + C c).roots = { x1, x2 } ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a :=
by
rw [roots_quadratic_eq_pair_iff_of_ne_zero ha]
field_simp
exact
and_congr ⟨fun h => by linear_combination h, fun h => by linear_combination h⟩
⟨fun h => by linear_combination -h, fun h => by linear_combination -h⟩
