R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
letI := Classical.decEq σ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees (f + g)) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
repeat' rw [degreeOf]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees f ⊔ degrees g) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees (f + g)) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
apply (Multiset.count_le_of_le n (degrees_add f g)).trans
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees f ∪ degrees g) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees f ⊔ degrees g) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
dsimp
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees f ∪ degrees g) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
rw [Multiset.count_union]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees (f + g)) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.308701
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees (f + g)) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
rw [degreeOf]