mdifferentiableAt_mul_left

Mathlib.Geometry.Manifold.Algebra.Monoid

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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