group — Mathlib

English

The quotient of a group by a congruence is a group with the induced operations.

Русский

Фактор-группа по конгруэнции образует группу с порожденными операциями.

LaTeX

$$$\\text{Group } c.Quotient$$$

Lean4

/-- The quotient of a group by a congruence relation is a group. -/
@[to_additive /-- The quotient of an `AddGroup` by an additive congruence relation is
    an `AddGroup`. -/
    ]
instance group : Group c.Quotient :=
  fast_instance%Function.Surjective.group Quotient.mk'' Quotient.mk''_surjective rfl (fun _ _ => rfl) (fun _ => rfl)
      (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl

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