apply_evalEquiv_symm_apply — Mathlib

English

For any m in M, evalEquiv(R,M)(m) equals Dual.eval(R,M)(m).

Русский

Для любого элемента m ∈ M отображение evalEquiv(R,M)(m) совпадает с Dual.eval(R,M)(m).

LaTeX

$$$$ \\mathrm{evalEquiv}\\ _R\\ M\\, (m) = \\mathrm{Dual.eval}\\ _R\\ M\\ (m). $$$$

Lean4

@[simp]
theorem apply_evalEquiv_symm_apply (f : Dual R M) (g : Dual R (Dual R M)) : f ((evalEquiv R M).symm g) = g f :=
  by
  set m := (evalEquiv R M).symm g
  rw [← (evalEquiv R M).apply_symm_apply g, evalEquiv_apply, Dual.eval_apply]

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