linMulLin_apply — Mathlib

English

Let f and g be linear maps from M to the base ring R. The bilinear form linMulLin f g is defined by (x, y) ↦ f(x) g(y). In particular, it satisfies (linMulLin f g)(x, y) = f(x) g(y) for all x, y ∈ M.

Русский

Пусть f и g — линейные отображения из M в R. Билинейная форма linMulLin f g задаётся как (x, y) ↦ f(x) g(y). В частности, для всех x, y ∈ M выполняется (linMulLin f g)(x, y) = f(x) g(y).

LaTeX

$$$ (\\mathrm{linMulLin}\\; f\\; g)(x,y) = f(x) \\cdot g(y) $$$

Lean4

@[simp]
theorem linMulLin_apply (x y) : linMulLin f g x y = f x * g y :=
  rfl

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