feat(data/polynomial/erase_lead): Characterizations of polynomials of…

… small support (#14500)

This PR adds iff-lemmas `card_support_eq_one`, `card_support_eq_two`, and `card_support_eq_three`. These will be useful for irreducibility of x^n-x-1.

src/data/polynomial/erase_lead.lean

@@ -273,4 +273,48 @@ lemma map_nat_degree_eq_nat_degree {S F : Type*} [semiring S]
   (φ p).nat_degree = p.nat_degree :=
 (map_nat_degree_eq_sub (λ f h, (nat.not_lt_zero _ h).elim) (by simpa)).trans p.nat_degree.sub_zero
 
+lemma card_support_eq_one : f.support.card = 1 ↔ ∃ (k : ℕ) (x : R) (hx : x ≠ 0), f = C x * X ^ k :=
+begin
+  refine ⟨λ h, _, _⟩,
+  { obtain hf := card_support_eq_zero.mp (erase_lead_card_support h),
+    refine ⟨f.nat_degree, f.leading_coeff, _, _⟩,
+    { rw [ne, leading_coeff_eq_zero, ←card_support_eq_zero, h],
+      exact one_ne_zero },
+    { conv_lhs { rw [←f.erase_lead_add_C_mul_X_pow, hf, zero_add] } } },
+  { rintros ⟨k, x, hx, rfl⟩,
+    rw [support_C_mul_X_pow k hx, card_singleton] },
+end
+
+lemma card_support_eq_two : f.support.card = 2 ↔ ∃ (k m : ℕ) (hkm : k < m)
+  (x y : R) (hx : x ≠ 0) (hy : y ≠ 0), f = C x * X ^ k + C y * X ^ m :=
+begin
+  refine ⟨λ h, _, _⟩,
+  { obtain ⟨k, x, hx, hf⟩ := card_support_eq_one.mp (erase_lead_card_support h),
+    refine ⟨k, f.nat_degree, _, x, f.leading_coeff, hx, _, _⟩,
+    { refine lt_of_le_of_lt _ (erase_lead_nat_degree_lt h.ge),
+      rw [hf, nat_degree_C_mul_X_pow k x hx] },
+    { rw [ne, leading_coeff_eq_zero, ←card_support_eq_zero, h],
+      exact two_ne_zero },
+    { rw [←hf, erase_lead_add_C_mul_X_pow] } },
+  { rintros ⟨k, m, hkm, x, y, hx, hy, rfl⟩,
+    exact card_support_binomial hkm.ne hx hy },
+end
+
+lemma card_support_eq_three : f.support.card = 3 ↔
+  ∃ (k m n : ℕ) (hkm : k < m) (hmn : m < n) (x y z : R) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0),
+    f = C x * X ^ k + C y * X ^ m + C z * X ^ n :=
+begin
+  refine ⟨λ h, _, _⟩,
+  { obtain ⟨k, m, hkm, x, y, hx, hy, hf⟩ := card_support_eq_two.mp (erase_lead_card_support h),
+    refine ⟨k, m, f.nat_degree, hkm, _, x, y, f.leading_coeff, hx, hy, _, _⟩,
+    { refine lt_of_le_of_lt _ (erase_lead_nat_degree_lt (le_trans (nat.le_succ 2) h.ge)),
+      rw [hf, nat_degree_add_eq_right_of_nat_degree_lt, nat_degree_C_mul_X_pow m y hy],
+      rwa [nat_degree_C_mul_X_pow k x hx, nat_degree_C_mul_X_pow m y hy] },
+    { rw [ne, leading_coeff_eq_zero, ←card_support_eq_zero, h],
+      exact three_ne_zero },
+    { rw [←hf, erase_lead_add_C_mul_X_pow] } },
+  { rintros ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩,
+    exact card_support_trinomial hkm hmn hx hy hz },
+end
+
 end polynomial