no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310892
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
classical
repeat' rw [degreeOf]
convert Multiset.count_le_of_le i (degrees_mul f g)
rw [Multiset.count_add]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310892
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees (f * g)) ≤ Multiset.count i (degrees f) + Multiset.count i (degrees g)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310892
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
repeat' rw [degreeOf]
case h.e'_4
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310892
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees f) + Multiset.count i (degrees g) = Multiset.count i (degrees f + degrees g)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310892
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees (f * g)) ≤ Multiset.count i (degrees f) + Multiset.count i (degrees g)
convert Multiset.count_le_of_le i (degrees_mul f g)
no goals
case h.e'_4
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310892
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees f) + Multiset.count i (degrees g) = Multiset.count i (degrees f + degrees g)
rw [Multiset.count_add]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310892
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees (f * g)) ≤ Multiset.count i (degrees f) + Multiset.count i (degrees g)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310892
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees (f * g)) ≤ Multiset.count i (degrees f) + Multiset.count i (degrees g)
rw [degreeOf]