coe_ofEquivFun — Mathlib

English

The coordinate map of Basis.ofEquivFun e equals the function e.symm on singletons: (Basis.ofEquivFun e) i = e.symm (Pi.single i 1).

Русский

Координатная карта Basis.ofEquivFun e равна применению обратного коду e.symm к единичному вектору Pi.single i 1.

LaTeX

$$$$ (Basis.ofEquivFun e) : ι → M = \lambda i. e^{-1}(\Pi_{i}^{ } 1) $$$$

Lean4

@[simp]
theorem coe_ofEquivFun [Finite ι] [DecidableEq ι] (e : M ≃ₗ[R] ι → R) :
    (Basis.ofEquivFun e : ι → M) = fun i => e.symm (Pi.single i 1) :=
  funext fun i => e.injective <| funext fun j => by simp [Basis.ofEquivFun, ← Finsupp.single_eq_pi_single]

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