mk_apply_apply — Mathlib

English

A deprecated variant: for field K and FiniteDimensional K W, B injective and B.flip injective produce a PerfectPairing with explicit left and right bijectivities.

Русский

Устаревшая версия: при поле K и FiniteDimensional K W билинейная форма B инъективна и B.flip инъективна даёт совершенную пару с явными биективностями слева и справа.

LaTeX

$$$\text{PerfectPairing}(K,V,W)$$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem mk_apply_apply {f : M →ₗ[R] N →ₗ[R] R} {hl} {hr} {x : M} : (⟨f, hl, hr⟩ : PerfectPairing R M N) x = f x :=
  rfl

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