mdifferentiableAt_mul_right

Mathlib.Geometry.Manifold.Algebra.Monoid

URI: https://scilib.ai/kg/mathlib#mdifferentiableAt_mul_right

English

For every a ∈ G and b ∈ G, the map x ↦ x · a is MDifferentiableAt I I at b.

Русский

Для любого a ∈ G и b ∈ G отображение x ↦ x · a является MDifferentiableAt I I в точке b.

LaTeX

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

Lean4

@[to_additive]
theorem mdifferentiableAt_mul_right {a b : G} : MDifferentiableAt I I (· * a) b :=
  contMDiffAt_mul_right.mdifferentiableAt le_rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru