mul_def — Mathlib

English

The product of two linear isometries corresponds to the product of their underlying functions.

Русский

Произведение двух линейных изометрий соответствует произведению их базовых функций.

LaTeX

$$Eq (LinearIsometry.instFunLike.coe (instHMul.hMul f g)) (Function.comp (LinearIsometry.instFunLike.coe f) (LinearIsometry.instFunLike.coe g))$$

Lean4

theorem mul_def (f g : E →ₗᵢ[R] E) : (f * g : E →ₗᵢ[R] E) = f.comp g :=
  rfl

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