basis_val — Mathlib

English

For i ∈ Fin n, the i-th basis vector equals X^i.

Русский

Для i ∈ Fin n i-ый вектор базиса равен X^i.

LaTeX

$$$ (\\text{basis } R\,n\,i) = X^i. $$$

Lean4

@[simp]
theorem basis_val : (basis R n i : R[X]) = X ^ (i : ℕ) :=
  by
  change _ = ((⟨X ^ (i : ℕ), mem_degreeLT.2 <| (degree_X_pow_le i).trans_lt <| Nat.cast_lt.2 i.is_lt⟩ : R[X]_n) : R[X])
  refine congr_arg _ (Basis.apply_eq_iff.2 <| Finsupp.ext fun j ↦ ?_)
  simp only [basis_repr, coeff_X_pow, eq_comm, Finsupp.single_apply, Fin.ext_iff]

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