coe_mul — Mathlib

English

The coercion map from ContMDiffMap to functions commutes with multiplication.

Русский

Коэрционное отображение из ContMDiffMap в функции совместимо с умножением.

LaTeX

$$$\text{Coeff: } \text{ContMDiffMap}(I,I',N,G,n) \to (C^n(I,N;I',G))\to G$ satisfies $\text{coe}(f*g) = \text{coe}(f) * \text{coe}(g)$.$$

Lean4

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

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