Theorems · Definition · commutative algebra

WittVector.liftFun

{p : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      [inst_1 : Fact (Nat.Prime p)] →
        {S : Type u_2} → [inst_2 : Semiring S] → ((k : ℕ) → S →+* TruncatedWittVector p k R) → S → WittVector p R

Given a family fₖ : S → TruncatedWittVector p k R and s : S, we produce a Witt vector by defining the kth entry to be the final entry of fₖ s.

Defined in

Mathlib.RingTheory.WittVector.Truncated

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFactSemiring