contMDiffAt_mul_right — Mathlib

English

For every a ∈ G, the map R_a: G → G defined by R_a(x) = x · a is ContMDiffAt I I n at every b ∈ G; i.e., right translation by a is smooth of the specified class.

Русский

Для любого элемента a ∈ G отображение R_a: G → G, заданное R_a(x) = x · a, является ContMDiffAt I I n в любой точке b ∈ G; то есть правое умножение на a гладко в заданном классе.

LaTeX

$$$\forall a,b \in G,\; \operatorname{ContMDiffAt} I I n (\lambda x. x \cdot a) b$$$

Lean4

@[to_additive]
theorem contMDiffAt_mul_right {a b : G} : ContMDiffAt I I n (· * a) b :=
  contMDiff_mul_right.contMDiffAt

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