map_right

Mathlib.GroupTheory.SemidirectProduct

URI: https://scilib.ai/kg/mathlib#SemidirectProduct.map_right

English

The left component of the map agrees with fn on the left coordinate.

Русский

Левая компонентa отображения совпадает с fn на левой координате.

LaTeX

$$$ map\_left(g) = fn(g.left) $$$

Lean4

@[simp]
theorem map_right (g : N₁ ⋊[φ₁] G₁) : (map fn fg h g).right = fg g.right :=
  rfl

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

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

Разделы

Аффилиация

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