∀ {M₀ : Type u_2} {A : Type u_7} [inst : MonoidWithZero M₀] [inst_1 : Zero A] [inst_2 : MulActionWithZero M₀ A]
  {ι : Type u_12} [inst_3 : DecidableEq ι] (x : A) (i j : ι), Pi.single i 1 j • x = Pi.single i x j