p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ vars (W_ R n) = range (n + 1)
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
⊢ vars (W_ R n) = range (n + 1)
have : ∀ i, (monomial (Finsupp.single i (p ^ (n - i))) ((p : R) ^ i)).vars = {i} := by
  intro i
  refine' vars_monomial_single i (pow_ne_zero _ hp.1) _
  rw [← Nat.cast_pow, Nat.cast_ne_zero]
  exact pow_ne_zero i hp.1
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ (Finset.biUnion (range (n + 1)) fun i => vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i))) = range (n + 1)

case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ Pairwise (Disjoint on fun i => vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)))
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ vars (W_ R n) = range (n + 1)
rw [wittPolynomial, vars_sum_of_disjoint]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
⊢ ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
intro i
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ ↑p ^ i ≠ 0
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
refine' vars_monomial_single i (pow_ne_zero _ hp.1) _
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ p ^ i ≠ 0
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ ↑p ^ i ≠ 0
rw [← Nat.cast_pow, Nat.cast_ne_zero]
no goals
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ p ^ i ≠ 0
exact pow_ne_zero i hp.1
no goals
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ (Finset.biUnion (range (n + 1)) fun i => vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i))) = range (n + 1)
simp only [this, biUnion_singleton_eq_self]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ Pairwise (Disjoint on fun i => {i})
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ Pairwise (Disjoint on fun i => vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)))
simp only [this]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
a b : ℕ
h : a ≠ b
⊢ (Disjoint on fun i => {i}) a b
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ Pairwise (Disjoint on fun i => {i})
intro a b h
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
a b : ℕ
h : a ≠ b
⊢ ¬a ∈ (fun i => {i}) b
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
a b : ℕ
h : a ≠ b
⊢ (Disjoint on fun i => {i}) a b
apply disjoint_singleton_left.mpr
no goals
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type ?u.157043
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
a b : ℕ
h : a ≠ b
⊢ ¬a ∈ (fun i => {i}) b
rwa [mem_singleton]