rightCoset_eq_iff — Mathlib

English

Two elements x, y lie in the same right coset of s if and only if y x^{-1} ∈ s.

Русский

Две элементы x, y лежат в одной правой косете подгруппы s тогда и только тогда, когда y x^{-1} ∈ s.

LaTeX

$$$s x = s y \iff y x^{-1} \in s$$$

Lean4

@[to_additive rightAddCoset_eq_iff]
theorem rightCoset_eq_iff {x y : α} : op x • (s : Set α) = op y • s ↔ y * x⁻¹ ∈ s :=
  by
  rw [Set.ext_iff]
  simp_rw [mem_rightCoset_iff, SetLike.mem_coe]
  constructor
  · intro h
    apply (h y).mpr
    rw [mul_inv_cancel]
    exact s.one_mem
  · intro h z
    rw [← inv_mul_cancel_left y x⁻¹]
    rw [← mul_assoc]
    exact s.mul_mem_cancel_right h

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