curry_mulSingle — Mathlib

English

Curry of the Pi-mulSingle with i ∈ ι×ι' and b ∈ M yields e.g. curry (Pi.mulSingle i b) = Pi.mulSingle i.1 (Pi.mulSingle i.2 b).

Русский

Карри-операция для Pi.mulSingle: карри (Pi.mulSingle i b) = Pi.mulSingle i.1 (Pi.mulSingle i.2 b).

LaTeX

$$$\text{curry}(\Pi.mulSingle i b) = \Pi.mulSingle i.1 (\Pi.mulSingle i.2 b)$$$

Lean4

@[to_additive (attr := simp)]
theorem curry_mulSingle (i : ι × ι') (b : M) : curry (Pi.mulSingle i b) = Pi.mulSingle i.1 (Pi.mulSingle i.2 b) :=
  curry_update _ _ _

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