Theorems · Theorem · number theory

WittVector.RecursionMain.succNthVal_spec

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0),
  (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot
    (WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂)

Defined in

Mathlib.RingTheory.WittVector.FrobeniusFractionField

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactFieldCharPIsAlgClosed