no goals
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ n
⊢ ↑(weightedHomogeneousComponent w n) φ = 0
classical
rw [weightedHomogeneousComponent_apply, sum_eq_zero]
intro d hd; rw [mem_filter] at hd
exfalso; exact h _ hd.1 hd.2
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ n
⊢ ∀ (x : σ →₀ ℕ), x ∈ Finset.filter (fun d => ↑(weightedDegree' w) d = n) (support φ) → ↑(monomial x) (coeff x φ) = 0
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ n
⊢ ↑(weightedHomogeneousComponent w n) φ = 0
rw [weightedHomogeneousComponent_apply, sum_eq_zero]
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ 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_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ 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_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ ↑(monomial d) (coeff d φ) = 0
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ Finset.filter (fun d => ↑(weightedDegree' w) d = n) (support φ)
⊢ ↑(monomial d) (coeff d φ) = 0
rw [mem_filter] at hd
case h
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ False
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ ↑(monomial d) (coeff d φ) = 0
exfalso
no goals
case h
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ↑(weightedDegree' w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ↑(weightedDegree' w) d = n
⊢ False
exact h _ hd.1 hd.2