English
A deprecated variant of mkOfInjective: under field K and FiniteDimensional K W, B injective and B.flip injective yield a perfect pairing.
Русский
Устаревшая версия mkOfInjective: при поле K и FiniteDimensional K W инъективность B и B.flip приводят к совершенной паре.
LaTeX
$$$\text{PerfectPairing}(K,V,W)$$$
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 form. -/
@[deprecated LinearMap.IsPerfPair.of_injective' (since := "2025-05-27")]
def mkOfInjective' {K V W : Type*} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
[FiniteDimensional K W] (B : V →ₗ[K] W →ₗ[K] K) (h : Injective B) (h' : Injective B.flip) : PerfectPairing K V W
where
toLinearMap := B
bijective_left :=
⟨h, by
have : FiniteDimensional K V := FiniteDimensional.of_injective B h
rwa [← B.flip_injective_iff₁]⟩
bijective_right := ⟨h', by rwa [← B.flip.flip_injective_iff₁, LinearMap.flip_flip]⟩
