English
The basisFun basis is canonically equivalent to the identity function on the function space; i.e., its equivalence to the identity is given by refl.
Русский
Базис basisFun канонически эквивалентен тождественному отображению на пространство функций; эквивалентность равна тождественному отображению.
LaTeX
$$$\text{basisFun_equivFun } : (\Pi.basisFun R η).equivFun = \text{LinearEquiv.refl } _ _$$$
Lean4
@[simp]
theorem basisFun_equivFun : (Pi.basisFun R η).equivFun = LinearEquiv.refl _ _ :=
Basis.equivFun_ofEquivFun _