basis_repr — Mathlib

English

For the basis built from bases b_i, the representation map evaluated at g and index ix equals (b_{ix.1}).repr (g_{ix.1}) (ix.2).

Русский

Для базиса, построенного из базисов b_i, отображение представления на элемент g и индекс ix даёт значение (b_{ix.1}).repr (g_{ix.1}) (ix.2).

LaTeX

$$$(\\mathrm{Finsupp}.basis\\; b).\\mathrm{repr}\; g\\; i_x = (b_{i_x.1}).\\mathrm{repr}(g_{i_x.1})\\; i_x.2$$$

Lean4

@[simp]
theorem basis_repr {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) (g : ι →₀ M) (ix) :
    (Finsupp.basis b).repr g ix = (b ix.1).repr (g ix.1) ix.2 :=
  rfl

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