case a
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ i ∈ vars (↑C a * φ) ↔ i ∈ vars φ
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
⊢ vars (↑C a * φ) = vars φ
ext1 i
case a
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ (∃ d, coeff d (↑C a * φ) ≠ 0 ∧ i ∈ d.support) ↔ ∃ d, coeff d φ ≠ 0 ∧ i ∈ d.support
case a
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ i ∈ vars (↑C a * φ) ↔ i ∈ vars φ
simp only [mem_vars, exists_prop, mem_support_iff]
case a.h
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ ∀ (a_1 : σ →₀ ℕ), coeff a_1 (↑C a * φ) ≠ 0 ∧ i ∈ a_1.support ↔ coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support
case a
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ (∃ d, coeff d (↑C a * φ) ≠ 0 ∧ i ∈ d.support) ↔ ∃ d, coeff d φ ≠ 0 ∧ i ∈ d.support
apply exists_congr
case a.h
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (↑C a * φ) ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
case a.h
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ ∀ (a_1 : σ →₀ ℕ), coeff a_1 (↑C a * φ) ≠ 0 ∧ i ∈ a_1.support ↔ coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support
intro d
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (↑C a * φ) ≠ 0 ↔ coeff d φ ≠ 0
case a.h
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (↑C a * φ) ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
apply and_congr _ Iff.rfl
no goals
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.169900
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (↑C a * φ) ≠ 0 ↔ coeff d φ ≠ 0
rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and_iff]