Theorems · Theorem · commutative algebra

WittVector.peval_polyOfInterest

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] (n : ℕ) (x y : WittVector p k),
  WittVector.peval (WittVector.polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)

Defined in

Mathlib.RingTheory.WittVector.MulCoeff

Cited by

1 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactCommRing