σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
⊢ ∀ (x : σ →₀ ℕ), x ∈ filter (fun d => ∑ i in d.support, ↑d i = n) (support φ) → ↑(monomial x) (coeff x φ) = 0
σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
⊢ ↑(homogeneousComponent n) φ = 0
rw [homogeneousComponent_apply, sum_eq_zero]
σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ filter (fun d => ∑ i in d.support, ↑d i = n) (support φ)
⊢ ↑(monomial d) (coeff d φ) = 0
σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
⊢ ∀ (x : σ →₀ ℕ), x ∈ filter (fun d => ∑ i in d.support, ↑d i = n) (support φ) → ↑(monomial x) (coeff x φ) = 0
intro d hd
σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ∑ i in d.support, ↑d i = n
⊢ ↑(monomial d) (coeff d φ) = 0
σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ filter (fun d => ∑ i in d.support, ↑d i = n) (support φ)
⊢ ↑(monomial d) (coeff d φ) = 0
rw [mem_filter] at hd
case h
σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ∑ i in d.support, ↑d i = n
⊢ False
σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ∑ i in d.support, ↑d i = n
⊢ ↑(monomial d) (coeff d φ) = 0
exfalso
no goals
case h
σ : Type u_1
τ : Type ?u.355900
R : Type u_2
S : Type ?u.355906
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ∑ i in d.support, ↑d i = n
⊢ False
exact h _ hd.1 hd.2