leftAdjointOfNondegenerate — Mathlib

English

For a nondegenerate B, an isomorphism ψ is adjoint to φ with respect to B if and only if ψ equals the left adjoint of φ with respect to B.

Русский

Для невырожденной B отображение ψ является сопряженным к φ по B тогда и только тогда, когда ψ равняется левому сопряженному φ по B.

LaTeX

$$$\\text{IsAdjointPair}(B,B,\\psi,\\phi) \\iff \\psi = B.leftAdjointOfNondegenerate b \\circ \\phi$$$

Lean4

/-- Given the nondegenerate bilinear form `B` and the linear map `φ`,
`leftAdjointOfNondegenerate` provides the left adjoint of `φ` with respect to `B`.
The lemma proving this property is `BilinForm.isAdjointPairLeftAdjointOfNondegenerate`. -/
noncomputable def leftAdjointOfNondegenerate (B : BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) : V →ₗ[K] V :=
  symmCompOfNondegenerate (B.compRight φ) B b

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