Theorems · Theorem · commutative algebra

xInTermsOfW_eq

∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p] {n : ℕ},
  xInTermsOfW p R n =
    (MvPolynomial.X n - ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) *
      MvPolynomial.C (⅟↑p ^ n)

Defined in

Mathlib.RingTheory.WittVector.WittPolynomial

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingInvertible