Theorems · Theorem · commutative algebra

WittVector.eq_of_apply_teichmuller_eq

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [inst : CommRing R] [CharP R p] [PerfectRing R p] {S : Type u_2}
  [inst_3 : CommRing S] (f g : WittVector p R →+* S),
  IsNilpotent ↑p → (∀ (x : R), f ((WittVector.teichmuller p) x) = g ((WittVector.teichmuller p) x)) → f = g

Given a ring S such that p is nilpotent in S and two ring maps f g : 𝕎 R →+* S, if they coincide on the teichmuller representatives, then they are equal.

Defined in

Mathlib.RingTheory.WittVector.TeichmullerSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactCommRingCharPPerfectRingCommRing