compRight_compLeft — Mathlib

English

Similarly, applying r to the second argument first and then l to the first yields the same bilinear form as B composed with l on the first argument and r on the second.

Русский

Аналогично, применение r ко второму аргументу затем l к первому даёт ту же билинейную форму, что и B после применения l к первому и r ко второму.

LaTeX

$$$ (B.compRight\, r).compLeft\, l \;=\; B.\;comp\, l\, r $$$

Lean4

@[simp]
theorem compRight_compLeft (B : BilinForm R M) (l r : M →ₗ[R] M) : (B.compRight r).compLeft l = B.comp l r :=
  rfl

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