English
Let R be a finite integral domain and f, g be quadratic polynomials in R[X]. If the size of R is odd, then there exist a, b in R such that f(a) + g(b) = 0.
Русский
Пусть R — конечное интегральное кольцо и f, g — квадратичные многочлены из R[X]. Если размер R нечетный, то существует пара элементов a, b из R такая, что f(a) + g(b) = 0.
LaTeX
$$$\exists a \in R \;\exists b \in R\; (f(a) + g(b) = 0)$$$
Lean4
/-- If `f` and `g` are quadratic polynomials, then the `f.eval a + g.eval b = 0` has a solution. -/
theorem exists_root_sum_quadratic [Fintype R] {f g : R[X]} (hf2 : degree f = 2) (hg2 : degree g = 2)
(hR : Fintype.card R % 2 = 1) : ∃ a b, f.eval a + g.eval b = 0 :=
letI := Classical.decEq R
suffices ¬Disjoint (univ.image fun x : R => eval x f) (univ.image fun x : R => eval x (-g))
by
simp only [disjoint_left, mem_image] at this
push_neg at this
rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩
exact ⟨a, b, by rw [ha, ← hb, eval_neg, neg_add_cancel]⟩
fun hd : Disjoint _ _ =>
lt_irrefl (2 * #((univ.image fun x : R => eval x f) ∪ univ.image fun x : R => eval x (-g))) <|
calc
2 * #((univ.image fun x : R => eval x f) ∪ univ.image fun x : R => eval x (-g)) ≤ 2 * Fintype.card R :=
Nat.mul_le_mul_left _ (Finset.card_le_univ _)
_ = Fintype.card R + Fintype.card R := (two_mul _)
_ < natDegree f * #(univ.image fun x : R => eval x f) + natDegree (-g) * #(univ.image fun x : R => eval x (-g)) :=
(add_lt_add_of_lt_of_le
(lt_of_le_of_ne (card_image_polynomial_eval (by rw [hf2]; decide))
(mt (congr_arg (· % 2)) (by simp [natDegree_eq_of_degree_eq_some hf2, hR])))
(card_image_polynomial_eval (by rw [degree_neg, hg2]; decide)))
_ = 2 * #((univ.image fun x : R => eval x f) ∪ univ.image fun x : R => eval x (-g)) :=
by
rw [card_union_of_disjoint hd]
simp [natDegree_eq_of_degree_eq_some hf2, natDegree_eq_of_degree_eq_some hg2, mul_add]
