Theorems · Definition · number theory

WittVector.RecursionMain.succNthVal

(p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst : Field k] →
        [CharP k p] →
          [IsAlgClosed k] → (n : ℕ) → (a₁ a₂ : WittVector p k) → (Fin (n + 1) → k) → a₁.coeff 0 ≠ 0 → a₂.coeff 0 ≠ 0 → k

This is the n+1st coefficient of our solution, projected from root_exists.

Defined in: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Cited by: 5 results in Mathlib
Foundations: Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fact Field CharP IsAlgClosed

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fieldstatement and proof · cited by 7,404
Factstatement and proof · cited by 2,726
Nat.Primestatement and proof · cited by 2,059
CharPstatement and proof · cited by 478
WittVectorstatement and proof · cited by 227
IsAlgClosedstatement and proof · cited by 150
WittVector.coeffstatement and proof · cited by 138
WittVector.RecursionMain.root_existsproof · cited by 1

Cited by6

Results whose statement or proof uses this declaration.

WittVector.frobeniusRotationCoeffproof · cited by 3
WittVector.RecursionMain.succNthVal_specstatement · cited by 1
WittVector.RecursionMain.succNthVal_spec'statement and proof · cited by 1
WittVector.frobenius_frobeniusRotationproof · cited by 1
WittVector.RecursionMain.succNthVal.congr_simpstatement and proof · cited by 0
WittVector.frobeniusRotationCoeff.eq_defstatement and proof · cited by 0