symm_dualMap_evalEquiv — Mathlib

English

The evaluation equivalence equals the evaluation map on the dual side, i.e., evalEquiv R M as a linear map equals Dual.eval R M.

Русский

Эквивалентность оценки равна отображению оценки на дуальном пространстве: evalEquiv R M как линейное отображение совпадает с Dual.eval R M.

LaTeX

$$$$ \\mathrm{evalEquiv}_{R,M} = \\mathrm{Dual.eval}_{R} M. $$$$

Lean4

@[simp]
theorem symm_dualMap_evalEquiv : (evalEquiv R M).symm.dualMap = Dual.eval R (Dual R M) := by ext; simp

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