finsupp_var — Mathlib

English

In the finsupp presentation, the i-th coordinate corresponds to the i-th generator with coefficient 1 at i and 0 elsewhere.

Русский

В презентации finsupp i-я координата соответствует i‑му генератору с коэффициентом 1 в i и нулём в остальных местах.

LaTeX

$$$\\text{finsupp pres ι}.\\text{var}\\langle i,g\\rangle = \\mathrm{Finsupp}.single i((pres.var g))$$$

Lean4

@[simp]
theorem finsupp_var (i : ι) (g : pres.G) : (finsupp pres ι).var ⟨i, g⟩ = Finsupp.single i (pres.var g) :=
  by
  apply (finsuppLequivDFinsupp A).injective
  erw [(finsuppLequivDFinsupp A).apply_symm_apply]
  rw [directSum_var, finsuppLequivDFinsupp_apply_apply, Finsupp.toDFinsupp_single]
  rfl

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