English
The smoothLeftMul construction provides a canonical smooth map sending g to the map x ↦ g x.
Русский
Конструкция smoothLeftMul задаёт гладкое отображение, отправляющее g в отображение x ↦ g x.
LaTeX
$$$\text{smoothLeftMul} : C^∞⟮I, G; I, G⟯$ with $\text{smoothLeftMul}(g)$ is the map $x \mapsto g x$$$
Lean4
@[scoped macro LieGroup.«term𝑹»]
public meta def «_aux_Mathlib_Geometry_Manifold_Algebra_Monoid___macroRules_LieGroup_term𝑹_1» : Macro✝ := fun
| `(𝑹) => ``(smoothRightMul)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
