bilinearComp_zero — Mathlib

English

If the second argument is zero, bilinearComp becomes zero: bilinearComp f (0 : E' →SL[σ₁'] E) gF = 0.

Русский

Если второй аргумент нулевой, bilinearComp равен нулю: bilinearComp f (0 : E' →SL[σ₁'] E) gF = 0.

LaTeX

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

Lean4

@[simp]
theorem bilinearComp_zero {gE : E' →SL[σ₁'] E} {gF : F' →SL[σ₂'] F} :
    bilinearComp (0 : E →SL[σ₁₃] F →SL[σ₂₃] G) gE gF = 0 :=
  rfl

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