English
On non-dependent functions, mulSingle i x i' equals x if i'=i and equals 1 otherwise; i.e., an ite representation.
Русский
На независимых от индекса функциях mulSingle i x i' равен x если i'=i, и 1 в противном случае; тождественное представление через if-then-else.
LaTeX
$$$(mulSingle i x) i' = \text{if } i' = i \text{ then } x \text{ else } 1$$$
Lean4
/-- On non-dependent functions, `Pi.mulSingle` can be expressed as an `ite` -/
@[to_additive /-- On non-dependent functions, `Pi.single` can be expressed as an `ite` -/
]
theorem mulSingle_apply (i : ι) (x : M) (i' : ι) : (mulSingle i x : ι → M) i' = if i' = i then x else 1 :=
Function.update_apply (1 : ι → M) i x i'
