Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: golf Polynomial.Degree.Definitions #10526

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: golf Polynomial.Degree.Definitions #10526

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 15 additions & 26 deletions Mathlib/Data/Polynomial/Degree/Definitions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,18 +140,9 @@ theorem degree_eq_iff_natDegree_eq {p : R[X]} {n : ℕ} (hp : p ≠ 0) :

theorem degree_eq_iff_natDegree_eq_of_pos {p : R[X]} {n : ℕ} (hn : 0 < n) :
p.degree = n ↔ p.natDegree = n := by
constructor
· intro H
rwa [← degree_eq_iff_natDegree_eq]
rintro rfl
rw [degree_zero] at H
exact Option.noConfusion H
· intro H
rwa [degree_eq_iff_natDegree_eq]
rintro rfl
rw [natDegree_zero] at H
rw [H] at hn
exact lt_irrefl _ hn
obtain rfl|h := eq_or_ne p 0
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure what the correct style is, but I've always been putting spaces around |.

Suggested change
obtain rfl|h := eq_or_ne p 0
obtain rfl | h := eq_or_ne p 0

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Both styles occur.

· simp [hn.ne]
· exact degree_eq_iff_natDegree_eq h
#align polynomial.degree_eq_iff_nat_degree_eq_of_pos Polynomial.degree_eq_iff_natDegree_eq_of_pos

theorem natDegree_eq_of_degree_eq_some {p : R[X]} {n : ℕ} (h : degree p = n) : natDegree p = n := by
Expand All @@ -172,9 +163,9 @@ theorem natDegree_eq_of_degree_eq [Semiring S] {q : S[X]} (h : degree p = degree
natDegree p = natDegree q := by unfold natDegree; rw [h]
#align polynomial.nat_degree_eq_of_degree_eq Polynomial.natDegree_eq_of_degree_eq

theorem le_degree_of_ne_zero (h : coeff p n ≠ 0) : (n : WithBot ℕ) ≤ degree p :=
show @LE.le (WithBot ℕ) _ (some n : WithBot ℕ) (p.support.sup some : WithBot ℕ) from
Finset.le_sup (mem_support_iff.2 h)
theorem le_degree_of_ne_zero (h : coeff p n ≠ 0) : (n : WithBot ℕ) ≤ degree p := by
rw [Nat.cast_withBot]
exact Finset.le_sup (mem_support_iff.2 h)
#align polynomial.le_degree_of_ne_zero Polynomial.le_degree_of_ne_zero

theorem le_natDegree_of_ne_zero (h : coeff p n ≠ 0) : n ≤ natDegree p := by
Expand Down Expand Up @@ -212,7 +203,7 @@ theorem supp_subset_range_natDegree_succ : p.support ⊆ Finset.range (natDegree

theorem degree_le_degree (h : coeff q (natDegree p) ≠ 0) : degree p ≤ degree q := by
by_cases hp : p = 0
· rw [hp]
· rw [hp, degree_zero]
exact bot_le
· rw [degree_eq_natDegree hp]
exact le_degree_of_ne_zero h
Expand Down Expand Up @@ -266,10 +257,8 @@ theorem degree_one_le : degree (1 : R[X]) ≤ (0 : WithBot ℕ) := by rw [← C_
theorem natDegree_C (a : R) : natDegree (C a) = 0 := by
by_cases ha : a = 0
· have : C a = 0 := by rw [ha, C_0]
rw [natDegree, degree_eq_bot.2 this]
rfl
· rw [natDegree, degree_C ha]
rfl
rw [natDegree, degree_eq_bot.2 this, WithBot.unbot'_bot]
· rw [natDegree, degree_C ha, WithBot.unbot_zero']
#align polynomial.nat_degree_C Polynomial.natDegree_C

@[simp]
Expand All @@ -286,7 +275,7 @@ theorem degree_nat_cast_le (n : ℕ) : degree (n : R[X]) ≤ 0 := degree_le_of_n

@[simp]
theorem degree_monomial (n : ℕ) (ha : a ≠ 0) : degree (monomial n a) = n := by
rw [degree, support_monomial n ha]; rfl
rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]
#align polynomial.degree_monomial Polynomial.degree_monomial

@[simp]
Expand All @@ -300,7 +289,7 @@ theorem degree_C_mul_X (ha : a ≠ 0) : degree (C a * X) = 1 := by

theorem degree_monomial_le (n : ℕ) (a : R) : degree (monomial n a) ≤ n :=
letI := Classical.decEq R
if h : a = 0 then by rw [h, (monomial n).map_zero]; exact bot_le
if h : a = 0 then by rw [h, (monomial n).map_zero, degree_zero]; exact bot_le
else le_of_eq (degree_monomial n h)
#align polynomial.degree_monomial_le Polynomial.degree_monomial_le

Expand Down Expand Up @@ -335,7 +324,7 @@ theorem natDegree_monomial_le (a : R) {m : ℕ} : (monomial m a).natDegree ≤ m
classical
rw [Polynomial.natDegree_monomial]
split_ifs
exacts [Nat.zero_le _, rfl.le]
exacts [Nat.zero_le _, le_rfl]
#align polynomial.nat_degree_monomial_le Polynomial.natDegree_monomial_le

theorem natDegree_monomial_eq (i : ℕ) {r : R} (r0 : r ≠ 0) : (monomial i r).natDegree = i :=
Expand Down Expand Up @@ -452,8 +441,8 @@ theorem eq_X_add_C_of_degree_le_one (h : degree p ≤ 1) : p = C (p.coeff 1) * X

theorem eq_X_add_C_of_degree_eq_one (h : degree p = 1) :
p = C p.leadingCoeff * X + C (p.coeff 0) :=
(eq_X_add_C_of_degree_le_one (show degree p ≤ 1 from h ▸ le_rfl)).trans
(by simp only [leadingCoeff, natDegree_eq_of_degree_eq_some h]; rfl)
(eq_X_add_C_of_degree_le_one h.le).trans
(by rw [← Nat.cast_one] at h; rw [leadingCoeff, natDegree_eq_of_degree_eq_some h])
#align polynomial.eq_X_add_C_of_degree_eq_one Polynomial.eq_X_add_C_of_degree_eq_one

theorem eq_X_add_C_of_natDegree_le_one (h : natDegree p ≤ 1) :
Expand Down Expand Up @@ -511,7 +500,7 @@ variable [Semiring R] [Nontrivial R] {p q : R[X]}

@[simp]
theorem degree_one : degree (1 : R[X]) = (0 : WithBot ℕ) :=
degree_C (show (1 : R) ≠ 0 from zero_ne_one.symm)
degree_C one_ne_zero
#align polynomial.degree_one Polynomial.degree_one

@[simp]
Expand Down
Loading