eq_of_right_mem_center

Mathlib.GroupTheory.Subgroup.Center

URI: https://scilib.ai/kg/mathlib#IsConj.eq_of_right_mem_center

English

If IsConj g h and h lies in the center, then g = h.

Русский

Если g и h конъюгируемы и h лежит в центре, то g = h.

LaTeX

$$$IsConj(g,h) \land h \in Z(M) \Rightarrow g = h$$$

Lean4

theorem eq_of_right_mem_center {g h : M} (H : IsConj g h) (Hh : h ∈ Set.center M) : g = h :=
  (H.symm.eq_of_left_mem_center Hh).symm

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

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

Разделы

Аффилиация

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