mem_doubleCoset_self — Mathlib

English

If b ∈ HaK, then HaK = HbK; i.e. a point lying in HaK identifies the same double coset as a.

Русский

Если b ∈ HaK, то HaK = HbK; то есть точка, лежащая в HaK, определяет ту же двойную косету, что и a.

LaTeX

$$$ b \\in H a K \\Rightarrow H b K = H a K $$$

Lean4

theorem mem_doubleCoset_self (H K : Subgroup G) (a : G) : a ∈ doubleCoset a H K :=
  mem_doubleCoset.mpr ⟨1, H.one_mem, 1, K.one_mem, (one_mul a).symm.trans (mul_one (1 * a)).symm⟩

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