[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑(expand R p) f = sum f fun e a => ↑C a * (X ^ p) ^ e
[PROOFSTEP]
simp [expand, eval₂]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
r : R
⊢ ↑(expand R p) (↑(monomial q) r) = ↑(monomial (q * p)) r
[PROOFSTEP]
simp_rw [← smul_X_eq_monomial, AlgHom.map_smul, AlgHom.map_pow, expand_X, mul_comm, pow_mul]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
r : R
⊢ ↑(expand R p) (↑(expand R q) (↑C r)) = ↑(expand R (p * q)) (↑C r)
[PROOFSTEP]
simp_rw [expand_C]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f✝ f g : R[X]
ihf : ↑(expand R p) (↑(expand R q) f) = ↑(expand R (p * q)) f
ihg : ↑(expand R p) (↑(expand R q) g) = ↑(expand R (p * q)) g
⊢ ↑(expand R p) (↑(expand R q) (f + g)) = ↑(expand R (p * q)) (f + g)
[PROOFSTEP]
simp_rw [AlgHom.map_add, ihf, ihg]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : ↑(expand R p) (↑(expand R q) (↑C r * X ^ n)) = ↑(expand R (p * q)) (↑C r * X ^ n)
⊢ ↑(expand R p) (↑(expand R q) (↑C r * X ^ (n + 1))) = ↑(expand R (p * q)) (↑C r * X ^ (n + 1))
[PROOFSTEP]
simp_rw [AlgHom.map_mul, expand_C, AlgHom.map_pow, expand_X, AlgHom.map_pow, expand_X, pow_mul]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑(expand R 0) f = ↑C (eval 1 f)
[PROOFSTEP]
simp [expand]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
r : R
⊢ ↑(expand R 1) (↑C r) = ↑C r
[PROOFSTEP]
rw [expand_C]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f✝ f g : R[X]
ihf : ↑(expand R 1) f = f
ihg : ↑(expand R 1) g = g
⊢ ↑(expand R 1) (f + g) = f + g
[PROOFSTEP]
rw [AlgHom.map_add, ihf, ihg]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : ↑(expand R 1) (↑C r * X ^ n) = ↑C r * X ^ n
⊢ ↑(expand R 1) (↑C r * X ^ (n + 1)) = ↑C r * X ^ (n + 1)
[PROOFSTEP]
rw [AlgHom.map_mul, expand_C, AlgHom.map_pow, expand_X, pow_one]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑(expand R (p ^ Nat.zero)) f = (↑(expand R p))^[Nat.zero] f
[PROOFSTEP]
rw [pow_zero, expand_one, Function.iterate_zero, id]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
n : ℕ
ih : ↑(expand R (p ^ n)) f = (↑(expand R p))^[n] f
⊢ ↑(expand R (p ^ Nat.succ n)) f = (↑(expand R p))^[Nat.succ n] f
[PROOFSTEP]
rw [Function.iterate_succ_apply', pow_succ, expand_mul, ih]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑derivative (↑(expand R p) f) = ↑(expand R p) (↑derivative f) * (↑p * X ^ (p - 1))
[PROOFSTEP]
rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_nat_cast, derivative_X, mul_one]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (↑(expand R p) f) n = if p ∣ n then coeff f (n / p) else 0
[PROOFSTEP]
simp only [expand_eq_sum]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (sum f fun e a => ↑C a * (X ^ p) ^ e) n = if p ∣ n then coeff f (n / p) else 0
[PROOFSTEP]
simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (∑ x in support f, if p * x = n then coeff f x else 0) = if p ∣ n then coeff f (n / p) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ (∑ x in support f, if p * x = n then coeff f x else 0) = coeff f (n / p)
[PROOFSTEP]
rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]
[GOAL]
case pos.h₀
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ∀ (b : ℕ), b ∈ support f → b ≠ n / p → (if p * b = n then coeff f b else 0) = 0
[PROOFSTEP]
intro b _ hb2
[GOAL]
case pos.h₀
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ support f
hb2 : b ≠ n / p
⊢ (if p * b = n then coeff f b else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case pos.h₀.hnc
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ support f
hb2 : b ≠ n / p
⊢ ¬p * b = n
[PROOFSTEP]
intro hb3
[GOAL]
case pos.h₀.hnc
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ support f
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ False
[PROOFSTEP]
apply hb2
[GOAL]
case pos.h₀.hnc
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ support f
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ b = n / p
[PROOFSTEP]
rw [← hb3, Nat.mul_div_cancel_left b hp]
[GOAL]
case pos.h₁
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ¬n / p ∈ support f → (if p * (n / p) = n then coeff f (n / p) else 0) = 0
[PROOFSTEP]
intro hn
[GOAL]
case pos.h₁
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : ¬n / p ∈ support f
⊢ (if p * (n / p) = n then coeff f (n / p) else 0) = 0
[PROOFSTEP]
rw [not_mem_support_iff.1 hn]
[GOAL]
case pos.h₁
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : ¬n / p ∈ support f
⊢ (if p * (n / p) = n then 0 else 0) = 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : ¬n / p ∈ support f
h✝ : p * (n / p) = n
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : ¬n / p ∈ support f
h✝ : ¬p * (n / p) = n
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ (∑ x in support f, if p * x = n then coeff f x else 0) = 0
[PROOFSTEP]
rw [Finset.sum_eq_zero]
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ ∀ (x : ℕ), x ∈ support f → (if p * x = n then coeff f x else 0) = 0
[PROOFSTEP]
intro k _
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ support f
⊢ (if p * k = n then coeff f k else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case neg.hnc
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ support f
⊢ ¬p * k = n
[PROOFSTEP]
exact fun hkn => h ⟨k, hkn.symm⟩
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (↑(expand R p) f) (n * p) = coeff f n
[PROOFSTEP]
rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (↑(expand R p) f) (p * n) = coeff f n
[PROOFSTEP]
rw [mul_comm, coeff_expand_mul hp]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q n : ℕ
hn : 0 < n
g g' : R[X]
H : ↑(expand R n) g = ↑(expand R n) g'
k : ℕ
⊢ coeff g k = coeff g' k
[PROOFSTEP]
rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ ↑(expand R p) f = ↑C r ↔ f = ↑C r
[PROOFSTEP]
rw [← expand_C, expand_inj hp, expand_C]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
cases' p.eq_zero_or_pos with hp hp
[GOAL]
case inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
[GOAL]
case inr
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
rw [hf, AlgHom.map_zero, natDegree_zero, zero_mul]
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
rw [← WithBot.coe_eq_coe]
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree (↑(expand R p) f)) = ↑(natDegree f * p)
[PROOFSTEP]
convert (degree_eq_natDegree hf1).symm
[GOAL]
case h.e'_3
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree f * p) = degree (↑(expand R p) f)
[PROOFSTEP]
symm
[GOAL]
case h.e'_3
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ degree (↑(expand R p) f) = ↑(natDegree f * p)
[PROOFSTEP]
refine' le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => _) _
[GOAL]
case h.e'_3.refine'_1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
⊢ coeff (↑(expand R p) f) n = 0
[PROOFSTEP]
rw [coeff_expand hp]
[GOAL]
case h.e'_3.refine'_1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
⊢ (if p ∣ n then coeff f (n / p) else 0) = 0
[PROOFSTEP]
split_ifs with hpn
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : p ∣ n
⊢ coeff f (n / p) = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt]
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : p ∣ n
⊢ natDegree f < n / p
[PROOFSTEP]
contrapose! hn
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ natDegree f
⊢ ↑n ≤ ↑(natDegree f * p)
[PROOFSTEP]
erw [WithBot.coe_le_coe, ← Nat.div_mul_cancel hpn]
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ natDegree f
⊢ ↑(n / p * p) ≤ natDegree f * p
[PROOFSTEP]
exact Nat.mul_le_mul_right p hn
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree f * p) ≤ degree (↑(expand R p) f)
[PROOFSTEP]
refine' le_degree_of_ne_zero _
[GOAL]
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ coeff (↑(expand R p) f) (Mul.mul (natDegree f) p) ≠ 0
[PROOFSTEP]
erw [coeff_expand_mul hp, ← leadingCoeff]
[GOAL]
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ leadingCoeff f ≠ 0
[PROOFSTEP]
exact mt leadingCoeff_eq_zero.1 hf
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : 0 < p
h : Monic f
⊢ Monic (↑(Polynomial.expand R p) f)
[PROOFSTEP]
rw [Monic.def, Polynomial.leadingCoeff, natDegree_expand, coeff_expand hp]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : 0 < p
h : Monic f
⊢ (if p ∣ natDegree f * p then coeff f (natDegree f * p / p) else 0) = 1
[PROOFSTEP]
simp [hp, h]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : p = 0
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
[PROOFSTEP]
ext
[GOAL]
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ coeff (map f (↑(expand R p) q)) n✝ = coeff (↑(expand S p) (map f q)) n✝
[PROOFSTEP]
rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]
[GOAL]
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ ↑f (if p ∣ n✝ then coeff q (n✝ / p) else 0) = if p ∣ n✝ then coeff (map f q) (n✝ / p) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : p ∣ n✝
⊢ ↑f (if p ∣ n✝ then coeff q (n✝ / p) else 0) = coeff (map f q) (n✝ / p)
[PROOFSTEP]
simp_all
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : ¬p ∣ n✝
⊢ ↑f (if p ∣ n✝ then coeff q (n✝ / p) else 0) = 0
[PROOFSTEP]
simp_all
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
⊢ eval r (↑(expand R p) P) = eval (r ^ p) P
[PROOFSTEP]
refine' Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => _) fun n a _ => by simp
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r a : R
⊢ eval r (↑(expand R p) (↑C a)) = eval (r ^ p) (↑C a)
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
n : ℕ
a : R
x✝ : eval r (↑(expand R p) (↑C a * X ^ n)) = eval (r ^ p) (↑C a * X ^ n)
⊢ eval r (↑(expand R p) (↑C a * X ^ (n + 1))) = eval (r ^ p) (↑C a * X ^ (n + 1))
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r (↑(expand R p) f) = eval (r ^ p) f
hg : eval r (↑(expand R p) g) = eval (r ^ p) g
⊢ eval r (↑(expand R p) (f + g)) = eval (r ^ p) (f + g)
[PROOFSTEP]
rw [AlgHom.map_add, eval_add, eval_add, hf, hg]
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
⊢ ↑(aeval r) (↑(expand R p) P) = ↑(aeval (r ^ p)) P
[PROOFSTEP]
refine' Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => _) fun n a _ => by simp
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
a : R
⊢ ↑(aeval r) (↑(expand R p) (↑C a)) = ↑(aeval (r ^ p)) (↑C a)
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
n : ℕ
a : R
x✝ : ↑(aeval r) (↑(expand R p) (↑C a * X ^ n)) = ↑(aeval (r ^ p)) (↑C a * X ^ n)
⊢ ↑(aeval r) (↑(expand R p) (↑C a * X ^ (n + 1))) = ↑(aeval (r ^ p)) (↑C a * X ^ (n + 1))
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : ↑(aeval r) (↑(expand R p) f) = ↑(aeval (r ^ p)) f
hg : ↑(aeval r) (↑(expand R p) g) = ↑(aeval (r ^ p)) g
⊢ ↑(aeval r) (↑(expand R p) (f + g)) = ↑(aeval (r ^ p)) (f + g)
[PROOFSTEP]
rw [AlgHom.map_add, aeval_add, aeval_add, hf, hg]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ coeff (contract p f) n = coeff f (n * p)
[PROOFSTEP]
simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt, ite_eq_left_iff]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ natDegree f + 1 ≤ n → 0 = coeff f (n * p)
[PROOFSTEP]
intro hn
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ 0 = coeff f (n * p)
[PROOFSTEP]
apply (coeff_eq_zero_of_natDegree_lt _).symm
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ natDegree f < n * p
[PROOFSTEP]
calc
  f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
  _ ≤ n * 1 := by simpa only [mul_one] using hn
  _ ≤ n * p := mul_le_mul_of_nonneg_left (show 1 ≤ p from hp.bot_lt) (zero_le n)
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ natDegree f + 1 ≤ n * 1
[PROOFSTEP]
simpa only [mul_one] using hn
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
hp : p ≠ 0
⊢ contract p (↑(expand R p) f) = f
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
hp : p ≠ 0
n✝ : ℕ
⊢ coeff (contract p (↑(expand R p) f)) n✝ = coeff f n✝
[PROOFSTEP]
simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt]
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
⊢ ↑(expand R p) (contract p f) = f
[PROOFSTEP]
ext n
[GOAL]
case a
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ coeff (↑(expand R p) (contract p f)) n = coeff f n
[PROOFSTEP]
rw [coeff_expand hp.bot_lt, coeff_contract hp]
[GOAL]
case a
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ (if p ∣ n then coeff f (n / p * p) else 0) = coeff f n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ coeff f (n / p * p) = coeff f n
[PROOFSTEP]
rw [Nat.div_mul_cancel h]
[GOAL]
case neg
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = coeff f n
[PROOFSTEP]
cases' n with n
[GOAL]
case neg.zero
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
h : ¬p ∣ Nat.zero
⊢ 0 = coeff f Nat.zero
[PROOFSTEP]
exact absurd (dvd_zero p) h
[GOAL]
case neg.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
have := coeff_derivative f n
[GOAL]
case neg.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
this : coeff (↑derivative f) n = coeff f (n + 1) * (↑n + 1)
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
rw [hf, coeff_zero, zero_eq_mul] at this 
[GOAL]
case neg.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
this : coeff f (n + 1) = 0 ∨ ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
cases' this with h'
[GOAL]
case neg.succ.inl
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : coeff f (n + 1) = 0
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
rw [h']
[GOAL]
case neg.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h✝ : ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
rename_i _ _ _ _ h'
[GOAL]
case neg.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h' 
[GOAL]
case neg.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : p ∣ Nat.succ n
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
exact absurd h' h
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
⊢ map (frobenius R p) (↑(expand R p) f) = f ^ p
[PROOFSTEP]
refine' f.induction_on' (fun a b ha hb => _) fun n a => _
[GOAL]
case refine'_1
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f a b : R[X]
ha : map (frobenius R p) (↑(expand R p) a) = a ^ p
hb : map (frobenius R p) (↑(expand R p) b) = b ^ p
⊢ map (frobenius R p) (↑(expand R p) (a + b)) = (a + b) ^ p
[PROOFSTEP]
rw [AlgHom.map_add, Polynomial.map_add, ha, hb, add_pow_char]
[GOAL]
case refine'_2
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) (↑(expand R p) (↑(monomial n) a)) = ↑(monomial n) a ^ p
[PROOFSTEP]
rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial, mul_pow, ← C.map_pow,
  frobenius_def]
[GOAL]
case refine'_2
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n : ℕ
a : R
⊢ ↑C (a ^ p) * X ^ (n * p) = ↑C (a ^ p) * (X ^ n) ^ p
[PROOFSTEP]
ring
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n : ℕ
⊢ map (frobenius R p ^ n) (↑(expand R (p ^ n)) f) = f ^ p ^ n
[PROOFSTEP]
induction' n with _ n_ih
[GOAL]
case zero
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
⊢ map (frobenius R p ^ Nat.zero) (↑(expand R (p ^ Nat.zero)) f) = f ^ p ^ Nat.zero
[PROOFSTEP]
simp [RingHom.one_def]
[GOAL]
case succ
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) (↑(expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ map (frobenius R p ^ Nat.succ n✝) (↑(expand R (p ^ Nat.succ n✝)) f) = f ^ p ^ Nat.succ n✝
[PROOFSTEP]
symm
[GOAL]
case succ
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) (↑(expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ f ^ p ^ Nat.succ n✝ = map (frobenius R p ^ Nat.succ n✝) (↑(expand R (p ^ Nat.succ n✝)) f)
[PROOFSTEP]
rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, RingHom.mul_def, ← map_map, mul_comm, expand_mul, ← map_expand]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
⊢ IsLocalRingHom ↑(expand R p)
[PROOFSTEP]
refine' ⟨fun f hf1 => _⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑↑(expand R p) f)
⊢ IsUnit f
[PROOFSTEP]
norm_cast at hf1 
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
⊢ IsUnit f
[PROOFSTEP]
have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
hf2 : ↑(expand R p) f = ↑C (coeff (↑(expand R p) f) 0)
⊢ IsUnit f
[PROOFSTEP]
rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2 
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
hf2 : ↑(expand R p) f = ↑C (coeff f 0)
⊢ IsUnit f
[PROOFSTEP]
rw [hf2, isUnit_C] at hf1 
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (coeff f 0)
hf2 : ↑(expand R p) f = ↑C (coeff f 0)
⊢ IsUnit f
[PROOFSTEP]
rw [expand_eq_C hp] at hf2 
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (coeff f 0)
hf2 : f = ↑C (coeff f 0)
⊢ IsUnit f
[PROOFSTEP]
rwa [hf2, isUnit_C]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible (↑(expand R (p ^ Nat.zero)) f)
⊢ Irreducible f
[PROOFSTEP]
rwa [pow_zero, expand_one] at hf 
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible (↑(expand R (p ^ n)) f) → Irreducible f
hf : Irreducible (↑(expand R (p ^ Nat.succ n)) f)
⊢ Irreducible (↑(expand R p) (↑(expand R (p ^ n)) f))
[PROOFSTEP]
rw [pow_succ] at hf 
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible (↑(expand R (p ^ n)) f) → Irreducible f
hf : Irreducible (↑(expand R (p * p ^ n)) f)
⊢ Irreducible (↑(expand R p) (↑(expand R (p ^ n)) f))
[PROOFSTEP]
rwa [expand_expand]
