instMul — Mathlib

English

There is a natural multiplication on ContMDiffMap giving a product map that is ContMDiffMap.

Русский

Существует естественное умножение для ContMDiffMap, задающее произведение карт и сохраняющее дифференцируемость.

LaTeX

$$$\text{instMul} : ContMDiffMap I I' N G n \times ContMDiffMap I I' N G n \to ContMDiffMap I I' N G n$$$

Lean4

@[to_additive]
protected instance instMul {G : Type*} [Mul G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' n G] :
    Mul C^n⟮I, N; I', G⟯ :=
  ⟨fun f g => ⟨f * g, f.contMDiff.mul g.contMDiff⟩⟩

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