Theorems · Theorem · commutative algebra

WittVector.init_pow

∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℕ) (x : WittVector p R) (n : ℕ),
  WittVector.init n (x ^ m) = WittVector.init n (WittVector.init n x ^ m)

Defined in

Mathlib.RingTheory.WittVector.InitTail

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFact