eq_iff_div_mem — Mathlib

English

In a group, for x,y ∈ G, (xN = yN) iff x y^{-1} ∈ N; this holds in general for any normal N or commutative groups.

Русский

Для элементов x, y в группе и нормальной N имеем xN = yN тогда и только тогда, когда x y^{-1} ∈ N.

LaTeX

$$$ \; (x : G \! / N) = y \; \Leftrightarrow \; x / y \in N $$$

Lean4

@[to_additive]
theorem eq_iff_div_mem {N : Subgroup G} [nN : N.Normal] {x y : G} : (x : G ⧸ N) = y ↔ x / y ∈ N :=
  by
  refine eq_comm.trans (QuotientGroup.eq.trans ?_)
  rw [nN.mem_comm_iff, div_eq_mul_inv]
    -- for commutative groups we don't need normality assumption

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