Theorems · Theorem · commutative algebra

WittVector.IsPoly.ext

∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f g : ⦃R : Type u⦄ → [CommRing R] → WittVector p R → WittVector p R},
  WittVector.IsPoly p f →
    WittVector.IsPoly p g →
      (∀ (R : Type u) [_Rcr : CommRing R] (x : WittVector p R) (n : ℕ),
          (WittVector.ghostComponent n) (f x) = (WittVector.ghostComponent n) (g x)) →
        ∀ (R : Type u) [_Rcr : CommRing R] (x : WittVector p R), f x = g x

Defined in

Mathlib.RingTheory.WittVector.IsPoly

Cited by

2 results in Mathlib

Foundations

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

Assumes

FactCommRing