comp_apply — Mathlib

English

Let B be a bilinear form on M. For any l, r : M → M and vectors v, w ∈ M, the value of the composed form at (v,w) equals B(l(v), r(w)).

Русский

Пусть B — билинейная форма на M. Для любых l, r : M → M и векторов v, w ∈ M, значение составленной формы в (v, w) равно B(l(v), r(w)).

LaTeX

$$$ (B.comp\, l\, r)(v, w) = B(l(v),\, r(w)) $$$

Lean4

@[simp]
theorem comp_apply (B : BilinForm R M') (l r : M →ₗ[R] M') (v w) : B.comp l r v w = B (l v) (r w) :=
  rfl

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