smul_comp' — Mathlib

English

Left multiplication by a C^n-scalar function commutes with composition of C^n maps: (f • g) ∘ h = (f ∘ h) • (g ∘ h).

Русский

Левое умножение на C^n-скалярную функцию сохраняет композицию: (f • g) ∘ h = (f ∘ h) • (g ∘ h).

LaTeX

$$$ (f\\cdot g)\\circ h = (f\\circ h)\\cdot (g\\circ h). $$$

Lean4

/-- The left multiplication with a `C^n` scalar function commutes with composition. -/
@[simp]
theorem smul_comp' {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V] (f : C^n⟮I'', N'; 𝕜⟯)
    (g : C^n⟮I'', N'; 𝓘(𝕜, V), V⟯) (h : C^n⟮I, N; I'', N'⟯) : (f • g).comp h = f.comp h • g.comp h :=
  rfl

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