smul — Mathlib

English

If a pair (f, g) is adjoint with respect to bilinear maps B and B', then scaling f and g by a scalar c preserves the adjoint relation; i.e., cf and cg remain adjoint with respect to B and B'.

Русский

Если пара (f, g) сопряжена относительно билинейных форм B и B', то умножение f и g на скаляр c сохраняет эту сопряжённость; cf и cg остаются сопряжёнными относительно B и B'.

LaTeX

$$$\\forall x,y$, B(cf(x))?y = B'(x)(cg(y)) \\,\\text{ whenever } B(f(x))\\,y = B'(x)(g(y))$$$

Lean4

theorem smul (c : R) (h : IsAdjointPair B B' f g) : IsAdjointPair B B' (c • f) (c • g) := fun _ _ ↦ by simp [h _]

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