toEndHom_apply

Mathlib.CategoryTheory.Action.Concrete

URI: https://scilib.ai/kg/mathlib#Action.FintypeCat.toEndHom_apply

English

The action endomorphism on the coset class ⟦h⟧ sends ⟦g⟧ to ⟦h g⁻¹⟧.

Русский

Действие эндоморфизм на классе смещения ⟦h⟧ отправляет ⟦g⟧ в ⟦h g⁻¹⟧.

LaTeX

$$$(toEndHom N g).hom (\overline{h}) = \overline{h g^{-1}}$$$

Lean4

@[simp]
theorem toEndHom_apply [N.Normal] (g h : G) : (toEndHom N g).hom ⟦h⟧ = ⟦h * g⁻¹⟧ :=
  rfl

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

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

Разделы

Аффилиация

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