uncurrySum_smul — Mathlib

English

A formula giving the value of the curryFinFinset-applied object in terms of the original map f and the Sum-based decomposition.

Русский

Формула для значения curryFinFinset в терминах оригинального отображения f и разложения через сумму.

LaTeX

$$$\\text{curryFinFinset}(R,M_2,M')\\!\\!\\;_{hk,hl} f (mk)(ml) = f (\\lambda i. Sum.elim mk ml (\\text{symm }(\\text{finSumEquivOfFinset } hk hl) i))$$$

Lean4

theorem uncurrySum_smul (r : R)
    (g : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
    uncurrySum (r • g) = r • uncurrySum g :=
  rfl

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