English
For any scalar k ∈ K and vector x ∈ M, the evaluation commutes with scalar multiplication: f.eval(k · x) = k · f.eval(x).
Русский
Для любого скаляра k ∈ K и вектора x ∈ M отображение f.eval умножается скаляром: f.eval(k·x) = k·f.eval(x).
LaTeX
$$$f( k\\cdot x ) = k\\cdot f(x)$$$
Lean4
theorem eval_smul [IsOrderedAddMonoid R] [Archimedean R] (k : K) (x : M) : f.eval (k • x) = k • f.eval x :=
by
by_cases hk : k = 0
· simp [hk]
unfold eval
rw [← toLex_smul, toLex.injective.eq_iff]
ext c
suffices f.evalCoeff (k • x) c = k • f.evalCoeff x c by simpa using this
by_cases h : ∃ y : f.val.domain, y.val - x ∈ ball K c
· obtain ⟨y, hy⟩ := h
have heq : (k • y).val - k • x = k • (y.val - x) := by simp [smul_sub]
have hy' : (k • y).val - k • x ∈ ball K c := by
rw [heq]
exact Submodule.smul_mem _ _ hy
simp [f.evalCoeff_eq hy, f.evalCoeff_eq hy', LinearPMap.map_smul]
have h' : ¬∃ y : f.val.domain, y.val - k • x ∈ ball K c :=
by
contrapose! h
obtain ⟨y, hy⟩ := h
use k⁻¹ • y
have heq : (k⁻¹ • y).val - x = k⁻¹ • (y.val - k • x) := by simp [smul_sub, smul_smul, inv_mul_cancel₀ hk]
exact heq ▸ Submodule.smul_mem _ _ hy
simp [f.evalCoeff_eq_zero h, f.evalCoeff_eq_zero h']
