compRight_apply — Mathlib

English

For a bilinear form B and a linear map f, the right-application formula holds: B.compRight f v w = B(v, f(w)).

Русский

Для билинейной формы B и линейного отображения f справедлива формула справа: B.compRight f v w = B(v, f(w)).

LaTeX

$$$ (B.compRight\, f)(v,w) = B(v, f(w)) $$$

Lean4

@[simp]
theorem compRight_apply (B : BilinForm R M) (f : M →ₗ[R] M) (v w) : B.compRight f v w = B v (f w) :=
  rfl

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