mul — Mathlib

English

If f,g form an adjoint pair with respect to B and B, and f',g' form an adjoint pair with respect to B and B, then the products ff' and g'g form an adjoint pair with respect to B and B.

Русский

Если пары (f,g) и (f',g') являются парами сопряжённости относительно одной и той же пары bilinear forms B и B, то произведения ff' и g'g образуют пару сопряжённости относительно B и B.

LaTeX

$$$IsAdjointPair(B,B)(f f',\\, g' g)$, given $IsAdjointPair(B,B,f,g)$ and $IsAdjointPair(B,B,f',g').$$$

Lean4

theorem mul {f g f' g' : Module.End R M} (h : IsAdjointPair B B f g) (h' : IsAdjointPair B B f' g') :
    IsAdjointPair B B (f * f') (g' * g) :=
  h'.comp h

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