coeff — Mathlib

English

If f: ℕ → R and hf expresses the Frobenius relation, then the map coeff(R,p,n) applied to ⟨f,hf⟩ returns f(n).

Русский

Если задана функция f: ℕ → R иhf задаёт отношение Фробениуса, то coeff(R,p,n) применённый к ⟨f,hf⟩ отдаёт f(n).

LaTeX

$$coeff(R,p,n) (⟨f,hf⟩) = f(n)$$

Lean4

/-- The `n`-th coefficient of an element of the perfection. -/
def coeff (n : ℕ) : Ring.Perfection R p →+* R where
  toFun f := f.1 n
  map_one' := rfl
  map_mul' _ _ := rfl
  map_zero' := rfl
  map_add' _ _ := rfl

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