case zero
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
⊢ vars (φ ^ Nat.zero) ⊆ vars φ

case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars (φ ^ Nat.succ n) ⊆ vars φ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
⊢ vars (φ ^ n) ⊆ vars φ
induction' n with n ih
no goals
case zero
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
⊢ vars (φ ^ Nat.zero) ⊆ vars φ
simp
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars (φ * φ ^ n) ⊆ vars φ
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars (φ ^ Nat.succ n) ⊆ vars φ
rw [pow_succ]
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars φ ∪ vars (φ ^ n) ⊆ vars φ
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars (φ * φ ^ n) ⊆ vars φ
apply Finset.Subset.trans (vars_mul _ _)
no goals
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.165103
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars φ ∪ vars (φ ^ n) ⊆ vars φ
exact Finset.union_subset (Finset.Subset.refl _) ih