rightCoset_mem_rightCoset — Mathlib

English

Let s be a subgroup of a group G and a ∈ s. Then the right coset s a equals s.

Русский

Пусть s — подгруппа группы G и a ∈ s. Тогда правая косета s a равна s.

LaTeX

$$$a \in s \implies s a = s$$$

Lean4

@[to_additive rightAddCoset_mem_rightAddCoset]
theorem rightCoset_mem_rightCoset {a : α} (ha : a ∈ s) : op a • (s : Set α) = s :=
  Set.ext fun b => by simp [mem_rightCoset_iff, mul_mem_cancel_right (s.inv_mem ha)]

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