coe_ofRepr — Mathlib

English

If e is a linear equivalence M ≃ ι → R, then the basis obtained by ofRepr e has i-th vector e.symm applied to the unit δ_i; equivalently, the i-th basis vector equals e^{-1}(δ_i).

Русский

Пусть e: M ≃_R ι →₀ R; полученный из e базис имеет i-ый вектор e.symm(δ_i), то есть тот же самый базис выражается через обращение к δ_i.

LaTeX

$$$(\mathrm{ofRepr}\ e)(i) = e^{-1}(\delta_i) = e.symm(\mathrm{Finsupp}.single i 1)$$$

Lean4

@[simp]
theorem coe_ofRepr (e : M ≃ₗ[R] ι →₀ R) : ⇑(ofRepr e) = fun i => e.symm (Finsupp.single i 1) :=
  rfl

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