con_subgroup — Mathlib

English

Con.subgroup yields a subgroup capturing the class of 1 under a congruence c.

Русский

Con.subgroup строит подгруппу, задаваемую классом 1 для конгруэнции c.

LaTeX

$$QuotientGroup.con c.subgroup = c$$

Lean4

@[to_additive (attr := simp)]
theorem con_subgroup (c : Con G) : QuotientGroup.con c.subgroup = c :=
  by
  ext x y
  rw [QuotientGroup.con, Con.rel_mk, leftRel_apply, Con.mem_subgroup_iff]
  exact ⟨fun h ↦ by simpa using c.mul (c.refl x) (c.symm h), fun h ↦ by simpa using c.mul (c.refl x⁻¹) (c.symm h)⟩

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