uncurry_mulSingle_mulSingle — Mathlib

English

Uncurry of the nested mulSingle equals the single Pi.mulSingle on the pair (i,i').

Русский

Развёртывание (uncurry) вложенного mulSingle даёт Pi.mulSingle на паре (i,i').

LaTeX

$$$\text{uncurry}(\Pi.mulSingle i (\Pi.mulSingle i' b)) = \Pi.mulSingle (i,i') b$$$

Lean4

@[to_additive (attr := simp)]
theorem uncurry_mulSingle_mulSingle (i : ι) (i' : ι') (b : M) :
    uncurry (Pi.mulSingle i (Pi.mulSingle i' b)) = Pi.mulSingle (i, i') b :=
  uncurry_update_update _ _ _ _

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