apply_apply_toDualRight_symm — Mathlib

English

For x ∈ M and f ∈ Dual R M, p(x) (p.toDualRight.symm f) = f(x).

Русский

Для x ∈ M и f ∈ Dual R M верно: p(x) (p.toDualRight.symm f) = f(x).

LaTeX

$$$(p x) (p.toDualRight.symm f) = f x$$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem apply_apply_toDualRight_symm (x : M) (f : Dual R M) : (p x) (p.toDualRight.symm f) = f x :=
  by
  have h := LinearEquiv.apply_symm_apply p.toDualRight f
  rw [toDualRight_apply] at h
  exact congrFun (congrArg DFunLike.coe h) x

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