English
Let u,v ≠ 0. Then Cu X^k + Cv X^l = Cu X^m + Cv X^n holds iff one of the three configurations holds: (k=m and l=n) or (u=v and k=n and l=m) or (u+v=0 and k=l and m=n).
Русский
Пусть u ≠ 0, v ≠ 0. Тогда Cu X^k + Cv X^l = Cu X^m + Cv X^n эквивалентно одному из трёх случаев: (k=m и l=n) или (u=v и k=n и l=m) или (u+v=0 и k=l и m=n).
LaTeX
$$$\forall k,l,m,n \; (u \neq 0) \land (v \neq 0) :\; Cu X^k + Cv X^l = Cu X^m + Cv X^n \iff (k=m \land l=n) \lor (u=v \land k=n \land l=m) \lor (u+v = 0 \land k=l \land m=n)$$$
Lean4
theorem binomial_eq_binomial {k l m n : ℕ} {u v : R} (hu : u ≠ 0) (hv : v ≠ 0) :
C u * X ^ k + C v * X ^ l = C u * X ^ m + C v * X ^ n ↔
k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n :=
by
simp_rw [C_mul_X_pow_eq_monomial, ← toFinsupp_inj, toFinsupp_add, toFinsupp_monomial]
exact Finsupp.single_add_single_eq_single_add_single hu hv
