ofEquivFun_repr_apply — Mathlib

English

For a finite index ι and a linear equivalence e, the i-th coordinate of x under the repr of Basis.ofEquivFun e equals e x i.

Русский

Для конечного индекса ι и линейного отображения e, i-я координата x по представлению Basis.ofEquivFun e равна e x i.

LaTeX

$$$$ (Basis.ofEquivFun e).repr x i = e x i $$$$

Lean4

@[simp]
theorem ofEquivFun_repr_apply [Finite ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) : (Basis.ofEquivFun e).repr x i = e x i :=
  rfl

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