frobeniusRotationCoeff — Mathlib

English

A specification for succNthVal: it satisfies a polynomial identity (the defining relation) with respect to a1, a2, bs.

Русский

Спецификация succNthVal: оно удовлетворяет полиномиальному тождеству относительно a1, a2, bs.

LaTeX

$$succNthVal_spec(p,n,a1,a2,bs,ha1,ha2) = IsRoot of succNthDefiningPoly evaluated at succNthVal$$

Lean4

/-- Recursively defines the sequence of coefficients for `WittVector.frobeniusRotation`. -/
noncomputable def frobeniusRotationCoeff {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : ℕ → k
  | 0 => solution p a₁ a₂
  | n + 1 => succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff ha₁ ha₂ i.val) ha₁ ha₂

Похожие утверждения