rightHom_splitting

Mathlib.GroupTheory.GroupExtension.Defs

URI: https://scilib.ai/kg/mathlib#GroupExtension.Splitting.rightHom_splitting

English

For every g in G, the right action of the splitting sends the image of g back to g, i.e., S.rightHom (s g) = g.

Русский

Для каждого g ∈ G правая работа разбиения отправляет образ g обратно в g: S.rightHom(σ(g)) = g.

LaTeX

$$$ S.rightHom(s(g)) = g \\quad (g \\in G) $$$

Lean4

@[to_additive (attr := simp)]
theorem rightHom_splitting (g : G) : S.rightHom (s g) = g :=
  s.rightInverse_rightHom g

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

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

Разделы

Аффилиация

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