Theorems · Definition · number theory

WittVector.frobeniusRotationCoeff

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

Recursively defines the sequence of coefficients for WittVector.frobeniusRotation.

Defined in

Mathlib.RingTheory.WittVector.FrobeniusFractionField

Cited by

3 results in Mathlib

Foundations

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

Assumes

FactFieldCharPIsAlgClosed