monoid — Mathlib

English

The quotient of a Monoid by a congruence is a Monoid with operation [a]·[b] = [ab].

Русский

Фактор-монойд по конгруэнции образуется моноидом с операцией [a]·[b] = [ab].

LaTeX

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

Lean4

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

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