basisFun_repr — Mathlib

English

The basisFun basis for functions on η is the same as the basis obtained from the equivalence with the identity map on η → R.

Русский

Базис basisFun для функций на η совпадает с базисом, полученным из тождественного отображения на η → R.

LaTeX

$$$\text{basisFun } R η = \text{Module.Basis.ofEquivFun (LinearEquiv.refl R (η \to R))}$$$

Lean4

@[simp]
theorem basisFun_repr (x : η → R) (i : η) : (Pi.basisFun R η).repr x i = x i := by simp [basisFun]

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