ofEquivFun — Mathlib

English

If e is a linear equivalence M ≃ ι → R, then the representation of the basis Basis.ofEquivFun e at x and i is e x i.

Русский

Пусть e: M ≃ ι → R — линейное эквивалентное отображение. Тогда дляBasis.ofEquivFun e представление в точке x и координате i равно e x i.

LaTeX

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

Lean4

/-- Define a basis by mapping each vector `x : M` to its coordinates `e x : ι → R`,
as long as `ι` is finite. -/
def ofEquivFun [Finite ι] (e : M ≃ₗ[R] ι → R) : Basis ι R M :=
  .ofRepr <| e.trans <| LinearEquiv.symm <| Finsupp.linearEquivFunOnFinite R R ι

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