compRight — Mathlib

English

Apply a linear map on both arguments of a bilinear form: B.comp l r is the bilinear form defined by (B.comp l r)(x,y) = B(l(x), r(y)).

Русский

Применение линейного отображения к обоим аргументам билинейной формы: B.comp l r задаёт форму (x,y) ↦ B(l(x), r(y)).

LaTeX

$$$$ (B.comp\ l\ r)(x,y) = B(l(x), r(y)). $$$$

Lean4

/-- Apply a linear map to the right argument of a bilinear form. -/
def compRight (B : BilinForm R M) (f : M →ₗ[R] M) : BilinForm R M :=
  B.comp LinearMap.id f

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