no goals
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ ↑(weightedHomogeneousComponent w n) φ = 0
classical
rw [weightedHomogeneousComponent_apply, sum_eq_zero]
intro d hd
rw [Finset.mem_filter] at hd
exfalso
apply lt_irrefl n
nth_rw 1 [← hd.2]
exact lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ ∀ (x : σ →₀ ℕ), x ∈ Finset.filter (fun d => ↑(weightedDegree' w) d = n) (support φ) → ↑(monomial x) (coeff x φ) = 0
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ ↑(weightedHomogeneousComponent w n) φ = 0
rw [weightedHomogeneousComponent_apply, sum_eq_zero]
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ Finset.filter (fun d => ↑(weightedDegree' w) d = n) (support φ)
⊢ ↑(monomial d) (coeff d φ) = 0
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ ∀ (x : σ →₀ ℕ), x ∈ Finset.filter (fun d => ↑(weightedDegree' w) d = n) (support φ) → ↑(monomial x) (coeff x φ) = 0
intro d hd
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ ↑(monomial d) (coeff d φ) = 0
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ Finset.filter (fun d => ↑(weightedDegree' w) d = n) (support φ)
⊢ ↑(monomial d) (coeff d φ) = 0
rw [Finset.mem_filter] at hd
case h
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ False
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ ↑(monomial d) (coeff d φ) = 0
exfalso
case h
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ n < n
case h
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ False
apply lt_irrefl n
case h
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ ↑(weightedDegree' w) d < n
case h
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ n < n
nth_rw 1 [← hd.2]
no goals
case h
R : Type u_2
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ ↑(weightedDegree' w) d < n
exact lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h