K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1))) ≤ ∑ s : σ, (Fintype.card K - 1) • {s}
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ degrees (indicator c) ≤ ∑ s : σ, (Fintype.card K - 1) • {s}
rw [indicator]
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (1 - (X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1))) ≤ ∑ s : σ, (Fintype.card K - 1) • {s}
refine' le_trans (degrees_prod _ _) (Finset.sum_le_sum fun s _ => _)
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees 1 ⊔ degrees ((X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (1 - (X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
refine' le_trans (degrees_sub _ _) _
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees ((X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees 1 ⊔ degrees ((X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
rw [degrees_one, ← bot_eq_zero, bot_sup_eq]
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s - ↑C (c s)) ≤ {s}
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees ((X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
refine' le_trans (degrees_pow _ _) (nsmul_le_nsmul_of_le_right _ _)
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s) ⊔ degrees (↑C (c s)) ≤ {s}
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s - ↑C (c s)) ≤ {s}
refine' le_trans (degrees_sub _ _) _
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s) ≤ {s}
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s) ⊔ degrees (↑C (c s)) ≤ {s}
rw [degrees_C, ← bot_eq_zero, sup_bot_eq]
no goals
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s) ≤ {s}
exact degrees_X' _