mk_smul — Mathlib

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]]

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