feat(data/polynomial/*): support_binomial and support_trinomial l…

…emmas (#14385)

This PR adds lemmas for the support of binomials and trinomials. The trinomial lemmas will be helpful for irreducibility of x^n-x-1.

src/data/polynomial/basic.lean

@@ -534,6 +534,8 @@ linear_map.to_add_monoid_hom_injective $ add_hom_ext $ λ n, linear_map.congr_fu
 lemma eq_zero_of_eq_zero (h : (0 : R) = (1 : R)) (p : R[X]) : p = 0 :=
 by rw [←one_smul R p, ←h, zero_smul]
 
+section fewnomials
+
 lemma support_monomial (n) {a : R} (H : a ≠ 0) : (monomial n a).support = singleton n :=
 by rw [←of_finsupp_single, support, finsupp.support_single_ne_zero H]
 
@@ -549,6 +551,23 @@ begin
   exact support_monomial' n c,
 end
 
+open finset
+
+lemma support_binomial' (k m : ℕ) (x y : R) : (C x * X ^ k + C y * X ^ m).support ⊆ {k, m} :=
+support_add.trans (union_subset ((support_C_mul_X_pow' k x).trans
+  (singleton_subset_iff.mpr (mem_insert_self k {m}))) ((support_C_mul_X_pow' m y).trans
+  (singleton_subset_iff.mpr (mem_insert_of_mem (mem_singleton_self m)))))
+
+lemma support_trinomial' (k m n : ℕ) (x y z : R) :
+  (C x * X ^ k + C y * X ^ m + C z * X ^ n).support ⊆ {k, m, n} :=
+support_add.trans (union_subset (support_add.trans (union_subset ((support_C_mul_X_pow' k x).trans
+  (singleton_subset_iff.mpr (mem_insert_self k {m, n}))) ((support_C_mul_X_pow' m y).trans
+  (singleton_subset_iff.mpr (mem_insert_of_mem (mem_insert_self m {n}))))))
+  ((support_C_mul_X_pow' n z).trans (singleton_subset_iff.mpr
+  (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n))))))
+
+end fewnomials
+
 lemma X_pow_eq_monomial (n) : X ^ n = monomial n (1:R) :=
 begin
   induction n with n hn,

src/data/polynomial/coeff.lean

@@ -134,6 +134,41 @@ lemma coeff_X_pow_self (n : ℕ) :
   coeff (X^n : R[X]) n = 1 :=
 by simp [coeff_X_pow]
 
+section fewnomials
+
+open finset
+
+lemma support_binomial {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
+  (C x * X ^ k + C y * X ^ m).support = {k, m} :=
+begin
+  apply subset_antisymm (support_binomial' k m x y),
+  simp_rw [insert_subset, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
+    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm,
+    mul_zero, zero_add, add_zero, ne.def, hx, hy, and_self, not_false_iff],
+end
+
+lemma support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0)
+  (hy : y ≠ 0) (hz : z ≠ 0) : (C x * X ^ k + C y * X ^ m + C z * X ^ n).support = {k, m, n} :=
+begin
+  apply subset_antisymm (support_trinomial' k m n x y z),
+  simp_rw [insert_subset, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
+    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne,
+    if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne',
+    mul_zero, add_zero, zero_add, ne.def, hx, hy, hz, and_self, not_false_iff],
+end
+
+lemma card_support_binomial {k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
+  (C x * X ^ k + C y * X ^ m).support.card = 2 :=
+by rw [support_binomial h hx hy, card_insert_of_not_mem (mt mem_singleton.mp h), card_singleton]
+
+lemma card_support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0)
+  (hy : y ≠ 0) (hz : z ≠ 0) : (C x * X ^ k + C y * X ^ m + C z * X ^ n).support.card = 3 :=
+by rw [support_trinomial hkm hmn hx hy hz, card_insert_of_not_mem
+  (mt mem_insert.mp (not_or hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
+  card_insert_of_not_mem (mt mem_singleton.mp hmn.ne), card_singleton]
+
+end fewnomials
+
 @[simp]
 theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
   coeff (p * polynomial.X ^ n) (d + n) = coeff p d :=