bilinearComp_apply — Mathlib

English

The bilinear composition with a zero first argument is the zero map: bilinearComp (0) gE gF = 0.

Русский

Билинейное композиционное отображение с нулевым первым аргументом равно нулю: bilinearComp (0) gE gF = 0.

LaTeX

$$$\operatorname{bilinearComp}(0, g_E, g_F) = 0$$$

Lean4

@[simp]
theorem bilinearComp_apply (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (gE : E' →SL[σ₁'] E) (gF : F' →SL[σ₂'] F) (x : E') (y : F') :
    f.bilinearComp gE gF x y = f (gE x) (gF y) :=
  rfl

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