basis_repr — Mathlib

English

For x ∈ S and i in Fin(natDegree f), the i-th coordinate of x with respect to the basis equals the i-th coefficient of modByMonicHom applied to x.

Русский

Для x ∈ S и i в Fin(natDegree f) i-я координата x по базису равна i-й коэффициенте полинома modByMonicHom применённого к x.

LaTeX

$$$ h.basis.repr\\, x\\, i = (h.modByMonicHom\\, x).coeff\\,(i : \\mathbb{N}) $$$

Lean4

@[simp]
theorem basis_repr (x : S) (i : Fin (natDegree f)) : h.basis.repr x i = (h.modByMonicHom x).coeff (i : ℕ) := by
  simp [IsAdjoinRootMonic.basis, toFinsupp_apply]

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