commGroup — Mathlib

English

The quotient of a CommGroup by a congruence is a CommGroup.

Русский

Фактор-комм-группа по конгруэнции образует комм-группу.

LaTeX

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

Lean4

/-- The quotient of a `CommGroup` by a congruence relation is a `CommGroup`. -/
@[to_additive /-- The quotient of an `AddCommGroup` by an additive congruence
    relation is an `AddCommGroup`. -/
    ]
instance commGroup {M : Type*} [CommGroup M] (c : Con M) : CommGroup c.Quotient :=
  fast_instance%Function.Surjective.commGroup _ Quotient.mk''_surjective rfl (fun _ _ => rfl) (fun _ => rfl)
      (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)

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