alternatizeUncurryFin_add — Mathlib

English

The construction alternatizeUncurryFin is additive in its argument f: alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g.

Русский

Конструкция alternatizeUncurryFin линейна по сумме, т.е. alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g.

LaTeX

$$$ alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g$$$

Lean4

@[simp]
theorem alternatizeUncurryFin_add (f g : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
    alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g :=
  by
  ext
  simp [alternatizeUncurryFin_apply, Finset.sum_add_distrib]

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