toLinHomFlip — Mathlib

English

The map toLinHomFlip takes a bilinear form A and yields a linear map whose action on x is the function y ↦ A(y,x).

Русский

Переобразование toLinHomFlip применимо к билинейной форме A и даёт линейное отображение, которое на x действует как y ↦ A(y,x).

LaTeX

$$$$ \text{toLinHomFlip}(A)(x) = (y \mapsto A(y,x)) . $$$$

Lean4

/-- The linear map obtained from a `BilinForm` by fixing the right co-ordinate and evaluating in
the left. -/
def toLinHomFlip : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R :=
  flipHom.toLinearMap

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