case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.265480
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
f : R →+* S
inst✝ : DecidableEq σ
i : σ
⊢ i ∈ vars p ↔ i ∈ Finset.biUnion (support p) Finsupp.support
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.265480
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
f : R →+* S
inst✝ : DecidableEq σ
⊢ vars p = Finset.biUnion (support p) Finsupp.support
ext i
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.265480
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
f : R →+* S
inst✝ : DecidableEq σ
i : σ
⊢ (∃ d x, i ∈ d.support) ↔ ∃ a, a ∈ support p ∧ i ∈ a.support
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.265480
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
f : R →+* S
inst✝ : DecidableEq σ
i : σ
⊢ i ∈ vars p ↔ i ∈ Finset.biUnion (support p) Finsupp.support
rw [mem_vars, Finset.mem_biUnion]
no goals
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.265480
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
f : R →+* S
inst✝ : DecidableEq σ
i : σ
⊢ (∃ d x, i ∈ d.support) ↔ ∃ a, a ∈ support p ∧ i ∈ a.support
simp