Theorem: Polynomial.degree_discConv_le (LeanCamCombi/DiscreteDeriv.lean)

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w P).degree ≤ P.degree
Tactic:
obtain rfl | hP := eq_or_ne P 0
State after:
case inl
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w 0).degree ≤ degree 0

case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hP : P ≠ 0
⊢ (discConv w P).degree ≤ P.degree

State before:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hP : P ≠ 0
⊢ (discConv w P).degree ≤ P.degree
Tactic:
refine degree_le_natDegree.trans $ (Nat.cast_le.2 natDegree_discConv_le).trans ?_
State after:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hP : P ≠ 0
⊢ ↑P.natDegree ≤ P.degree

State before:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hP : P ≠ 0
⊢ ↑P.natDegree ≤ P.degree
Tactic:
rw [degree_eq_natDegree hP]
State after:
no goals

State before:
case inl
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w 0).degree ≤ degree 0
Tactic:
simp
State after:
no goals