From 1dcf891c82dbc7df398cc6ff81ea46afc8ea43a2 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Wed, 25 May 2022 22:10:47 -0700 Subject: [PATCH] lemmas --- src/data/polynomial/basic.lean | 19 ++++++++++++++++++ src/data/polynomial/coeff.lean | 35 ++++++++++++++++++++++++++++++++++ 2 files changed, 54 insertions(+) diff --git a/src/data/polynomial/basic.lean b/src/data/polynomial/basic.lean index 220021bd25e4a..dba4825500cdd 100644 --- a/src/data/polynomial/basic.lean +++ b/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, diff --git a/src/data/polynomial/coeff.lean b/src/data/polynomial/coeff.lean index 2599b7c07ebe5..67df4cd5a7e6f 100644 --- a/src/data/polynomial/coeff.lean +++ b/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 :=