mdifferentiable_mul_left — Mathlib

English

For every a ∈ G, the map L_a: G → G defined by L_a(x) = a · x is MDifferentiable (of class I) everywhere.

Русский

Для любого a ∈ G отображение L_a: G → G, L_a(x) = a · x, является MDifferentiable повсеместно.

LaTeX

$$$\forall a \in G,\; MDifferentiable I I (\lambda x. a \cdot x)$$$

Lean4

@[to_additive]
theorem mdifferentiable_mul_left {a : G} : MDifferentiable I I (a * ·) :=
  contMDiff_mul_left.mdifferentiable le_rfl

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