of_injective' — Mathlib

English

If K is a field, M,N are vector spaces with FiniteDimensional K M, and p : M →ₗ[K] N →ₗ[K] K is such that p and p.flip are injective, then p is a perfect pairing.

Русский

Если K — поле, M,N — векторные пространства с FiniteDimensional K M, и p : M →ₗ[K] N →ₗ[K] K такова, что p и p.flip инъективны, то p — совершенная пара.

LaTeX

$$$p.IsPerfPair$$$

Lean4

/-- If the coefficients are a field, and one of the spaces is finite-dimensional, it is sufficient
to check only injectivity instead of bijectivity of the bilinear pairing. -/
theorem of_injective' [FiniteDimensional K N] (h : Injective p) (h' : Injective p.flip) : p.IsPerfPair :=
  .flip <| .of_injective h' h

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