coeff_frobenius — Mathlib

English

The nth coefficient of Frobenius x equals the evaluation of FrobeniusPoly at the coefficient sequence of x.

Русский

n-й коэффициент Frobenius x равен значениям FrobeniusPoly на последовательности коэффициентов x.

LaTeX

$$$$\operatorname{coeff}(\operatorname{frobenius}(x),n) = \mathrm{aeval}_{x.coeff}(\operatorname{frobeniusPoly}(p,n)).$$$$

Lean4

theorem coeff_frobenius (x : 𝕎 R) (n : ℕ) : coeff (frobenius x) n = MvPolynomial.aeval x.coeff (frobeniusPoly p n) :=
  coeff_frobeniusFun _ _

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