subgroup — Mathlib

English

The subgroup associated to a congruence c is defined by { x ∈ G | c x 1 }.

Русский

Подгруппа, соответствующая конгруэнции c, задаётся как { x ∈ G | c x 1 }.

LaTeX

$$Con.subgroup (c) = { x ∈ G | c x 1 }$$

Lean4

/-- The subgroup defined by the class of `1` for a congruence relation on a group.
-/
@[to_additive /-- The `AddSubgroup` defined by the class of `0` for an additive congruence relation
    on an `AddGroup`. -/
    ]
protected def _root_.Con.subgroup (c : Con G) : Subgroup G
    where
  carrier := {x | c x 1}
  one_mem' := c.refl 1
  mul_mem' hx hy := by simpa using c.mul hx hy
  inv_mem' h := by simpa using c.inv h

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