uncurrySum_apply — Mathlib

English

Scalar multiplication commutes with uncurrySum: uncurrySum (r • g) = r • uncurrySum g.

Русский

Скалярное умножение взаимодействует с uncurrySum: uncurrySum (r • g) = r • uncurrySum g.

LaTeX

$$$\\text{uncurrySum}(r \\cdot g) = r \\cdot \\text{uncurrySum}(g)$$$

Lean4

@[simp]
theorem uncurrySum_apply (g : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂))
    (u) : g.uncurrySum u = g (fun i ↦ u (.inl i)) (fun i' ↦ u (.inr i')) :=
  rfl

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