no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.52567
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ degrees (↑(map f) p) ⊆ degrees p
classical
dsimp only [degrees]
apply Multiset.subset_of_le
apply Finset.sup_mono
apply MvPolynomial.support_map_subset
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.52567
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ (Finset.sup (support (↑(map f) p)) fun s => ↑toMultiset s) ⊆ Finset.sup (support p) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.52567
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ degrees (↑(map f) p) ⊆ degrees p
dsimp only [degrees]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.52567
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ (Finset.sup (support (↑(map f) p)) fun s => ↑toMultiset s) ≤ Finset.sup (support p) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.52567
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ (Finset.sup (support (↑(map f) p)) fun s => ↑toMultiset s) ⊆ Finset.sup (support p) fun s => ↑toMultiset s
apply Multiset.subset_of_le
case a.h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.52567
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ support (↑(map f) p) ⊆ support p
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.52567
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ (Finset.sup (support (↑(map f) p)) fun s => ↑toMultiset s) ≤ Finset.sup (support p) fun s => ↑toMultiset s
apply Finset.sup_mono
no goals
case a.h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.52567
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ support (↑(map f) p) ⊆ support p
apply MvPolynomial.support_map_subset