eq_class_eq_leftCoset — Mathlib

English

The set of x with x ≡ g (mod s) equals the left coset g s.

Русский

Множество x таких, что x эквивалентно g по модулю s, равно левой косете g s.

LaTeX

$$$\{x \in \alpha : x \equiv g \pmod{s}\} = g s$$$

Lean4

@[to_additive]
theorem eq_class_eq_leftCoset (s : Subgroup α) (g : α) : {x : α | (x : α ⧸ s) = g} = g • s :=
  Set.ext fun z => by rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]

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