English
Scalar multiplication distributes across the mk construction: mk s (c • x) = c • mk s x.
Русский
Скалярное умножение распределяется через конструктор mk: mk s (c • x) = c • mk s x.
LaTeX
$$$$ \\mathrm{mk}\\,s\\,(c \\cdot x) = c \\cdot \\mathrm{mk}\\,s\\,x $$$$
Lean4
@[simp]
theorem mk_smul {s : Finset ι} (c : γ) (x : ∀ i : (↑s : Set ι), β (i : ι)) : mk s (c • x) = c • mk s x :=
ext fun i => by simp only [smul_apply, mk_apply]; split_ifs <;> [rfl; rw [smul_zero]]