rightHom_map

Mathlib.GroupTheory.GroupExtension.Defs

URI: https://scilib.ai/kg/mathlib#GroupExtension.Equiv.rightHom_map

English

An equivalence maps the inclusion of N compatibly: equiv (S.inl n) = S'.inl n.

Русский

Эквивалентность переводит вложение N совместимо: equiv(S.inl n) = S'.inl n.

LaTeX

$$$equiv (S.inl n) = S'.inl n$$$

Lean4

@[to_additive (attr := simp)]
theorem rightHom_map (e : E) : S'.rightHom (equiv e) = S.rightHom e :=
  congrFun equiv.rightHom_comm e

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

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

Разделы

Аффилиация

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