smoothLeftMul — Mathlib

English

Left multiplication by a fixed element g ∈ G defines a smooth map, i.e., the left multiplication map is C^∞ from I to I on G.

Русский

Левое умножение на фиксированный элемент g ∈ G задаёт гладкое отображение; левая умножение есть C^∞ от I к I на G.

LaTeX

$$$\text{smoothLeftMul} : C^∞⟮I, G; I, G⟯,\; x \mapsto g x$$$

Lean4

/-- Left multiplication by `g`. It is meant to mimic the usual notation in Lie groups.
Used mostly through the notation `𝑳`.
Lemmas involving `smoothLeftMul` with the notation `𝑳` usually use `L` instead of `𝑳` in the
names. -/
def smoothLeftMul : C^∞⟮I, G; I, G⟯ :=
  ⟨(g * ·), contMDiff_mul_left⟩

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