From 769f5fc4260b4f998bf7a2105a4d15594509c8ce Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 10 Aug 2023 12:07:45 +0000 Subject: [PATCH] feat: simple lemmas about polynomials and their degrees (#6220) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221). The signature of a theorem changed: ```lean theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : (p ^ m).coeff (n * m) = p.coeff n ^ m -- <-- the order of the product was `n * m` (p ^ m).coeff (m * n) = p.coeff n ^ m -- <-- and it became `m * n` ``` Modified files: ``` Data/Polynomial/Basic.lean Data/Polynomial/Degree/Lemmas.lean Data/Polynomial/Degree/Definitions.lean Data/Polynomial/Coeff.lean -- for a "`simp` can prove this" golf ``` --- Mathlib/Data/Polynomial/Basic.lean | 4 ++++ Mathlib/Data/Polynomial/Coeff.lean | 5 +---- Mathlib/Data/Polynomial/Degree/Definitions.lean | 14 ++++++++++++++ Mathlib/Data/Polynomial/Degree/Lemmas.lean | 14 +++++++++++--- 4 files changed, 30 insertions(+), 7 deletions(-) diff --git a/Mathlib/Data/Polynomial/Basic.lean b/Mathlib/Data/Polynomial/Basic.lean index 60de2217f538e..f7401151b897b 100644 --- a/Mathlib/Data/Polynomial/Basic.lean +++ b/Mathlib/Data/Polynomial/Basic.lean @@ -729,6 +729,10 @@ theorem coeff_C_zero : coeff (C a) 0 = a := theorem coeff_C_ne_zero (h : n ≠ 0) : (C a).coeff n = 0 := by rw [coeff_C, if_neg h] #align polynomial.coeff_C_ne_zero Polynomial.coeff_C_ne_zero +@[simp] +theorem coeff_nat_cast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0 := by + simp only [← C_eq_nat_cast, coeff_C, Nat.cast_ite, Nat.cast_zero] + theorem C_mul_X_pow_eq_monomial : ∀ {n : ℕ}, C a * X ^ n = monomial n a | 0 => mul_one _ | n + 1 => by diff --git a/Mathlib/Data/Polynomial/Coeff.lean b/Mathlib/Data/Polynomial/Coeff.lean index 7740b4f2eeecd..ffa58f4fadf40 100644 --- a/Mathlib/Data/Polynomial/Coeff.lean +++ b/Mathlib/Data/Polynomial/Coeff.lean @@ -370,11 +370,8 @@ end Coeff section cast -@[simp] theorem nat_cast_coeff_zero {n : ℕ} {R : Type _} [Semiring R] : (n : R[X]).coeff 0 = n := by - induction' n with n ih - · simp - · simp [ih] + simp only [coeff_nat_cast_ite, ite_true] #align polynomial.nat_cast_coeff_zero Polynomial.nat_cast_coeff_zero @[norm_cast] -- @[simp] -- Porting note: simp can prove this diff --git a/Mathlib/Data/Polynomial/Degree/Definitions.lean b/Mathlib/Data/Polynomial/Degree/Definitions.lean index cac6c3b81b08a..af71b1d474bf6 100644 --- a/Mathlib/Data/Polynomial/Degree/Definitions.lean +++ b/Mathlib/Data/Polynomial/Degree/Definitions.lean @@ -1077,6 +1077,20 @@ theorem coeff_pow_mul_natDegree (p : R[X]) (n : ℕ) : exact coeff_mul_degree_add_degree _ _ #align polynomial.coeff_pow_mul_nat_degree Polynomial.coeff_pow_mul_natDegree +theorem coeff_mul_add_eq_of_natDegree_le {df dg : ℕ} {g : R[X]} + (hdf : natDegree f ≤ df) (hdg : natDegree g ≤ dg) : + (f * g).coeff (df + dg) = f.coeff df * g.coeff dg := by + rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)] + · rw [Finset.Nat.mem_antidiagonal] + rintro ⟨df', dg'⟩ hmem hne + obtain h | hdf' := lt_or_le df df' + · rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul] + obtain h | hdg' := lt_or_le dg dg' + · rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero] + obtain ⟨rfl, rfl⟩ := + eq_and_eq_of_le_of_le_of_add_le hdf' hdg' (Finset.Nat.mem_antidiagonal.1 hmem).ge + exact (hne rfl).elim + theorem zero_le_degree_iff : 0 ≤ degree p ↔ p ≠ 0 := by rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot] #align polynomial.zero_le_degree_iff Polynomial.zero_le_degree_iff diff --git a/Mathlib/Data/Polynomial/Degree/Lemmas.lean b/Mathlib/Data/Polynomial/Degree/Lemmas.lean index 67a5ab1c9c1e2..198e580cd3198 100644 --- a/Mathlib/Data/Polynomial/Degree/Lemmas.lean +++ b/Mathlib/Data/Polynomial/Degree/Lemmas.lean @@ -173,14 +173,22 @@ theorem coeff_mul_of_natDegree_le (pm : p.natDegree ≤ m) (qn : q.natDegree ≤ #align polynomial.coeff_mul_of_nat_degree_le Polynomial.coeff_mul_of_natDegree_le theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : - (p ^ m).coeff (n * m) = p.coeff n ^ m := by + (p ^ m).coeff (m * n) = p.coeff n ^ m := by induction' m with m hm · simp - · rw [pow_succ', pow_succ', ← hm, Nat.mul_succ, coeff_mul_of_natDegree_le _ pn] - refine' natDegree_pow_le.trans (le_trans _ (mul_comm _ _).le) + · rw [pow_succ', pow_succ', ← hm, Nat.succ_mul, coeff_mul_of_natDegree_le _ pn] + refine' natDegree_pow_le.trans (le_trans _ (le_refl _)) exact mul_le_mul_of_nonneg_left pn m.zero_le #align polynomial.coeff_pow_of_nat_degree_le Polynomial.coeff_pow_of_natDegree_le +theorem coeff_pow_eq_ite_of_natDegree_le_of_le {o : ℕ} + (pn : natDegree p ≤ n) (mno : m * n ≤ o) : + coeff (p ^ m) o = if o = m * n then (coeff p n) ^ m else 0 := by + rcases eq_or_ne o (m * n) with rfl | h + · simpa only [ite_true] using coeff_pow_of_natDegree_le pn + · simpa only [h, ite_false] using coeff_eq_zero_of_natDegree_lt $ + lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm) + theorem coeff_add_eq_left_of_lt (qn : q.natDegree < n) : (p + q).coeff n = p.coeff n := (coeff_add _ _ _).trans <| (congr_arg _ <| coeff_eq_zero_of_natDegree_lt <| qn).trans <| add_zero _