fpowerSeriesBilinear_apply_two — Mathlib

English

The second coefficient in the bilinear power-series expansion equals the bilinear form itself: fpowerSeriesBilinear x 2 = f.uncurryBilinear.

Русский

Второй коэффициент в разложении равен самой билинейной форме: fpowerSeriesBilinear x 2 = f.uncurryBilinear.

LaTeX

$$$ f.fpowerSeriesBilinear x 2 = f.uncurryBilinear $$$

Lean4

@[simp]
theorem fpowerSeriesBilinear_apply_two (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    fpowerSeriesBilinear f x 2 = f.uncurryBilinear :=
  rfl

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