p : ℕ
R : Type ?u.533445
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = ↑C (1 / ↑p ^ n) * (wittStructureRat p Φ n * ↑C (↑p ^ n))
p : ℕ
R : Type ?u.533445
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n =
    ↑C (1 / ↑p ^ n) *
      (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
calc
  wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
  _ = _ := by rw [wittStructureRat_rec_aux]
case h
p : ℕ
R : Type ?u.533445
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0
p : ℕ
R : Type ?u.533445
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = ↑C (1 / ↑p ^ n) * (wittStructureRat p Φ n * ↑C (↑p ^ n))
rw [mul_left_comm, ← C_mul, div_mul_cancel, C_1, mul_one]
no goals
case h
p : ℕ
R : Type ?u.533445
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0
exact pow_ne_zero _ (Nat.cast_ne_zero.2 hp.1.ne_zero)
no goals
p : ℕ
R : Type ?u.533445
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑C (1 / ↑p ^ n) * (wittStructureRat p Φ n * ↑C (↑p ^ n)) =
    ↑C (1 / ↑p ^ n) *
      (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
rw [wittStructureRat_rec_aux]