English
A version of Pi.single_smul for non-dependent functions: single i (r • x) = r • single i x for functions M ↦ β.
Русский
Версия Pi.single_smul для не зависимых функций: single i (r • x) = r • single i x.
LaTeX
$$$\text{For non-dependent } M,\; \operatorname{single}_i(r\cdot x) = r\cdot \operatorname{single}_i x.$$$
Lean4
/-- A version of `Pi.single_smul` for non-dependent functions. It is useful in cases where Lean
fails to apply `Pi.single_smul`. -/
theorem single_smul' {α β} [Monoid α] [AddMonoid β] [DistribMulAction α β] [DecidableEq I] (i : I) (r : α) (x : β) :
single (M := fun _ => β) i (r • x) = r • single (M := fun _ => β) i x :=
single_smul (f := fun _ => β) i r x
