mul_comp — Mathlib

English

Composition respects multiplication: (f*g).comp h = f.comp h * g.comp h.

Русский

Сцепление сохраняет умножение: (f*g).comp h = f.comp h * g.comp h.

LaTeX

$$$(f * g).comp h = f.comp h * g.comp h$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_comp {G : Type*} [Mul G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' n G]
    (f g : C^n⟮I'', N'; I', G⟯) (h : C^n⟮I, N; I'', N'⟯) : (f * g).comp h = f.comp h * g.comp h :=
  rfl

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