mk_eq_of_doubleCoset_eq

Mathlib.GroupTheory.DoubleCoset

URI: https://scilib.ai/kg/mathlib#DoubleCoset.mk_eq_of_doubleCoset_eq

← MathLib Explorer

English

mk_eq_of_doubleCoset_eq: If doubleCoset a H K = doubleCoset b H K, then mk H K a = mk H K b.

Русский

Если HaK = HbK, то mk a = mk b.

LaTeX

$$$ HaK = HbK \\Rightarrow \\mathrm{mk}_{H,K}(a) = \\mathrm{mk}_{H,K}(b) $$$

Lean4

theorem mk_eq_of_doubleCoset_eq {H K : Subgroup G} {a b : G} (h : doubleCoset a H K = doubleCoset b H K) :
    mk H K a = mk H K b := by
  rw [eq]
  exact mem_doubleCoset.mp (h.symm ▸ mem_doubleCoset_self H K b)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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