contMDiff_mul — Mathlib

English

The map (p, q) ↦ p.q (multiplication) is ContMDiff from G × G to G given ContMDiffMul I n G.

Русский

Карта умножения из G × G в G является ContMDiff при условии ContMDiffMul I n G.

LaTeX

$$$$ \text{contMDiff} \bigl(\, \lambda p : G \times G, p_1 p_2 \bigr) \text{ holds under } [ContMDiffMul I n G]. $$$$

Lean4

@[to_additive]
theorem contMDiff_mul [ContMDiffMul I n G] : ContMDiff (I.prod I) I n fun p : G × G => p.1 * p.2 :=
  ContMDiffMul.contMDiff_mul

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