Theorems · Theorem · commutative algebra

WittVector.truncate_lift

∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  {f : (k : ℕ) → S →+* TruncatedWittVector p k R}
  (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) (s : S),
  (WittVector.truncate n) ((WittVector.lift f f_compat) s) = (f n) s

Defined in

Mathlib.RingTheory.WittVector.Truncated

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFactSemiring