toDualLeft_of_toDualRight_symm — Mathlib

English

For all x ∈ M and f ∈ Dual R M, p.toDualLeft x evaluated at p.toDualRight.symm f equals f(x).

Русский

Для всех x ∈ M и f ∈ Dual R M, значение p.toDualLeft x в p.toDualRight.symm f равно f(x).

LaTeX

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

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem toDualLeft_of_toDualRight_symm (x : M) (f : Dual R M) : (p.toDualLeft x) (p.toDualRight.symm f) = f x :=
  by
  rw [@toDualLeft_apply]
  exact apply_apply_toDualRight_symm p x f

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