eq — Mathlib · SciLib

English

Let a and b be elements of a group G and s a subgroup. In the quotient G / s the cosets of a and b are equal if and only if a^{-1} b ∈ s.

Русский

Пусть G — группа, s — подгруппа. Косеты a s и b s в фактор-группе G / s совпадают тогда и только тогда, когда a^{-1} b ∈ s.

LaTeX

$$$(a : \alpha \backslash s) = b \;\Longleftrightarrow\; a^{-1} b \in s$$$

Lean4

@[to_additive]
protected theorem eq {a b : α} : (a : α ⧸ s) = b ↔ a⁻¹ * b ∈ s :=
  calc
    _ ↔ leftRel s a b := Quotient.eq''
    _ ↔ _ := by rw [leftRel_apply]

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