From 41626f7d6f841571268fc92b28bd879386c99541 Mon Sep 17 00:00:00 2001 From: negiizhao Date: Wed, 7 Sep 2022 13:23:09 +0000 Subject: [PATCH] feat(data/polynomial/degree/definitions): add `degree_X_sub_C_le` (#16404) --- src/data/polynomial/algebra_map.lean | 2 +- src/data/polynomial/degree/definitions.lean | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/data/polynomial/algebra_map.lean b/src/data/polynomial/algebra_map.lean index a94b9adb93fda..296dde611bffa 100644 --- a/src/data/polynomial/algebra_map.lean +++ b/src/data/polynomial/algebra_map.lean @@ -375,7 +375,7 @@ begin have bound := calc (p * (X - C r)).nat_degree ≤ p.nat_degree + (X - C r).nat_degree : nat_degree_mul_le - ... ≤ p.nat_degree + 1 : add_le_add_left nat_degree_X_sub_C_le _ + ... ≤ p.nat_degree + 1 : add_le_add_left (nat_degree_X_sub_C_le _) _ ... < p.nat_degree + 2 : lt_add_one _, rw sum_over_range' _ _ (p.nat_degree + 2) bound, swap, diff --git a/src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/definitions.lean index 164821fa1cea1..87273d4ba7f5f 100644 --- a/src/data/polynomial/degree/definitions.lean +++ b/src/data/polynomial/degree/definitions.lean @@ -1047,10 +1047,11 @@ calc degree (p - q) = degree (erase (nat_degree q) p + -erase (nat_degree q) q) : degree_neg (erase (nat_degree q) q) ▸ degree_add_le _ _ ... < degree p : max_lt_iff.2 ⟨hd' ▸ degree_erase_lt hp0, hd.symm ▸ degree_erase_lt hq0⟩ +lemma degree_X_sub_C_le (r : R) : (X - C r).degree ≤ 1 := +(degree_sub_le _ _).trans (max_le degree_X_le (degree_C_le.trans zero_le_one)) -lemma nat_degree_X_sub_C_le {r : R} : (X - C r).nat_degree ≤ 1 := -nat_degree_le_iff_degree_le.2 $ le_trans (degree_sub_le _ _) $ max_le degree_X_le $ -le_trans degree_C_le $ with_bot.coe_le_coe.2 zero_le_one +lemma nat_degree_X_sub_C_le (r : R) : (X - C r).nat_degree ≤ 1 := +nat_degree_le_iff_degree_le.2 $ degree_X_sub_C_le r lemma degree_sub_eq_left_of_degree_lt (h : degree q < degree p) : degree (p - q) = degree p := by { rw ← degree_neg q at h, rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h] }