comp_comp — Mathlib

English

Apply a bilinear form to the left and right coordinates after composing with linear maps; i.e., comp (B : BilinForm R M) (l r) yields B(l(·), r(·)).

Русский

Применить билинейную форму к левому и правому аргументам после композиции с линейными отображениями; т.е. comp B l r задаёт B(l(·), r(·)).

LaTeX

$$$$ B^{\text{comp}}(x,y) = B(l(x), r(y)). $$$$

Lean4

theorem comp_comp {M'' : Type*} [AddCommMonoid M''] [Module R M''] (B : BilinForm R M'') (l r : M →ₗ[R] M')
    (l' r' : M' →ₗ[R] M'') : (B.comp l' r').comp l r = B.comp (l'.comp l) (r'.comp r) :=
  rfl

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