[GOAL]
σ : Type u
R : Type v
inst✝¹ : CommRing R
p m : ℕ
inst✝ : CharP R p
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n
[PROOFSTEP]
rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange ↑f (_ : ↑f 0 = 0) p = ↑(map f) p
[PROOFSTEP]
change Finsupp.mapRange (f : R →+ S) (f : R →+ S).map_zero p = map f p
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) p = ↑(map f) p
[PROOFSTEP]
rw [p.as_sum, Finsupp.mapRange_finset_sum, (map f).map_sum]
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ ∑ x in support p, Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) (↑(monomial x) (coeff x p)) =
    ∑ x in support p, ↑(map f) (↑(monomial x) (coeff x p))
[PROOFSTEP]
refine' Finset.sum_congr rfl fun n _ => _
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ support p
⊢ Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) (↑(monomial n) (coeff n p)) = ↑(map f) (↑(monomial n) (coeff n p))
[PROOFSTEP]
rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ support p
⊢ ↑(monomial n) (↑↑f (coeff n p)) = ↑(monomial n) (↑f (coeff n p))
[PROOFSTEP]
simp_all only [AddMonoidHom.coe_coe]
[GOAL]
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ totalDegree p ≤ m
[PROOFSTEP]
rw [totalDegree, Finset.sup_le_iff]
[GOAL]
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ ∀ (b : σ →₀ ℕ), b ∈ support p → (Finsupp.sum b fun x e => e) ≤ m
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n
[PROOFSTEP]
rw [restrictDegree, Finsupp.mem_supported]
[GOAL]
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
n : ℕ
⊢ ↑p.support ⊆ {n_1 | ∀ (i : σ), ↑n_1 i ≤ n} ↔ ∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
R : Type v
inst✝¹ : CommRing R
p✝ m : ℕ
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i (degrees p) ≤ n
[PROOFSTEP]
simp only [mem_restrictDegree, degrees_def, Multiset.count_finset_sup, Finsupp.count_toMultiset, Finset.sup_le_iff]
[GOAL]
σ : Type u
R : Type v
inst✝¹ : CommRing R
p✝ m : ℕ
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ (∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n) ↔ ∀ (i : σ) (b : σ →₀ ℕ), b ∈ support p → ↑b i ≤ n
[PROOFSTEP]
exact ⟨fun h n s hs => h s hs n, fun h s hs n => h n s hs⟩
