p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x in range (n + 1), if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑constantCoeff (W_ R n) = 0
simp only [wittPolynomial, map_sum, constantCoeff_monomial]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x in range (n + 1), if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
rw [sum_eq_zero]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ (if single i (p ^ (n - i)) = 0 then ↑p ^ i else 0) = 0
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
rintro i _
case hnc
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ (if single i (p ^ (n - i)) = 0 then ↑p ^ i else 0) = 0
rw [if_neg]
case hnc
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0
case hnc
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0
rw [Finsupp.single_eq_zero]
no goals
case hnc
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.75140
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0
exact ne_of_gt (pow_pos hp.1.pos _)