map_equiv_eq_comap_symm

Mathlib.Algebra.Group.Subgroup.Map

URI: https://scilib.ai/kg/mathlib#Subgroup.map_equiv_eq_comap_symm

English

For f: N ≃ G and K ⊆ G, K.comap f = K.map f.symm.

Русский

Для изоморфизма f: N ≃ G и подгруппы K ⊆ G верно K.comap f = K.map f.symm.

LaTeX

$$$K.comap f = K.map f^{-1}.$$$

Lean4

@[to_additive]
theorem map_equiv_eq_comap_symm (f : G ≃* N) (K : Subgroup G) : K.map f = K.comap (G := N) f.symm :=
  map_equiv_eq_comap_symm' _ _

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

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

Разделы

Аффилиация

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