equivFun_ofEquivFun — Mathlib

English

Equivalence between the basis constructed from e and the original e: (Basis.ofEquivFun e).equivFun = e.

Русский

Эквивалентность между базисом, построенным по e, и самой e: (Basis.ofEquivFun e).equivFun = e.

LaTeX

$$$$ (Basis.ofEquivFun e).equivFun = e $$$$

Lean4

@[simp]
theorem equivFun_ofEquivFun [Finite ι] (e : M ≃ₗ[R] ι → R) : (Basis.ofEquivFun e).equivFun = e :=
  by
  ext j
  simp_rw [Basis.equivFun_apply, Basis.ofEquivFun_repr_apply]

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