basis_repr — Mathlib

English

Let i be an index in Fin n and P ∈ R[X]_n. The i-th coordinate of P with respect to the standard basis {1, X, ..., X^{n-1}} equals the coefficient of X^i in P.

Русский

Пусть i — индекс в Fin n, и P ∈ R[X]_n. i-ая координата P по стандартному базису {1, X, ..., X^{n-1}} равна коэффициенту при X^i в P.

LaTeX

$$$\\text{coeff}_i(P) = ((\\text{basis } R\,n).repr\\,P)(i) \\quad(\\text{for } i = 0,1,...,n-1).$$$

Lean4

@[simp]
theorem basis_repr : (basis R n).repr P i = (P : R[X]).coeff i :=
  rfl

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