subgroupCongr_symm_apply

Mathlib.Algebra.Group.Subgroup.Map

URI: https://scilib.ai/kg/mathlib#MulEquiv.subgroupCongr_symm_apply

English

The inverse map of subgroupCongr also acts as the identity on elements when H=K.

Русский

Обратная карта subgroupCongr также является тождественной на элементах при H=K.

LaTeX

$$$((\\operatorname{subgroupCongr}\\, h).\\mathrm{symm} x : G) = x$$$

Lean4

@[to_additive (attr := simp)]
theorem subgroupCongr_symm_apply (h : H = K) (x) : ((MulEquiv.subgroupCongr h).symm x : G) = x :=
  rfl

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

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

Разделы

Аффилиация

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