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(Data/Polynomial/Degree/Definition): golf #6214

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(Data/Polynomial/Degree/Definition): golf #6214

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
13 changes: 6 additions & 7 deletions Mathlib/Data/Polynomial/Degree/Definitions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,10 +150,14 @@ theorem degree_eq_iff_natDegree_eq_of_pos {p : R[X]} {n : ℕ} (hn : 0 < n) :
#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 :=
have hp0 : p ≠ 0 := fun hp0 => by rw [hp0] at h; exact Option.noConfusion h
Option.some_inj.1 <| show (natDegree p : WithBot ℕ) = n by rwa [← degree_eq_natDegree hp0]
-- Porting note: `Nat.cast_withBot` is required.
by rw [natDegree, h, Nat.cast_withBot, WithBot.unbot'_coe]
#align polynomial.nat_degree_eq_of_degree_eq_some Polynomial.natDegree_eq_of_degree_eq_some

theorem degree_ne_of_natDegree_ne {n : ℕ} : p.natDegree ≠ n → degree p ≠ n :=
mt natDegree_eq_of_degree_eq_some
#align polynomial.degree_ne_of_nat_degree_ne Polynomial.degree_ne_of_natDegree_ne

@[simp]
theorem degree_le_natDegree : degree p ≤ natDegree p :=
WithBot.giUnbot'Bot.gc.le_u_l _
Expand Down Expand Up @@ -209,11 +213,6 @@ theorem degree_le_degree (h : coeff q (natDegree p) ≠ 0) : degree p ≤ degree
exact le_degree_of_ne_zero h
#align polynomial.degree_le_degree Polynomial.degree_le_degree

theorem degree_ne_of_natDegree_ne {n : ℕ} : p.natDegree ≠ n → degree p ≠ n :=
-- Porting note: `Nat.cast_withBot` is required.
mt fun h => by rw [natDegree, h, Nat.cast_withBot, WithBot.unbot'_coe]
#align polynomial.degree_ne_of_nat_degree_ne Polynomial.degree_ne_of_natDegree_ne

theorem natDegree_le_iff_degree_le {n : ℕ} : natDegree p ≤ n ↔ degree p ≤ n :=
WithBot.unbot'_bot_le_iff
#align polynomial.nat_degree_le_iff_degree_le Polynomial.natDegree_le_iff_degree_le
Expand Down
Loading