R_mul

Mathlib.Geometry.Manifold.Algebra.Monoid

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

← MathLib Explorer

English

Right translations respect composition: R_{gh} = R_h ∘ R_g.

Русский

Правые преобразования по gh равны композиции R_h ∘ R_g.

LaTeX

$$$R_{gh} = R_h \circ R_g$$$

Lean4

@[simp]
theorem R_mul {G : Type*} [Semigroup G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I ∞ G] (g h : G) :
    𝑹 I (g * h) = (𝑹 I h).comp (𝑹 I g) := by
  ext
  simp only [ContMDiffMap.comp_apply, R_apply, mul_assoc]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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