commMonoid — Mathlib

English

The quotient of a Commutative Monoid by a congruence is a Commutative Monoid.

Русский

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

LaTeX

$$$([a]_{c})\\cdot([b]_{c}) = ([b]_{c})\\cdot([a]_{c})$$$

Lean4

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

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