Theorems · Definition · group theory

Monoid.coprodCon

(M : Type u_1) → (N : Type u_2) → [MulOneClass M] → [MulOneClass N] → Con (FreeMonoid (M ⊕ N))

The minimal congruence relation c on FreeMonoid (M ⊕ N) such that FreeMonoid.of ∘ Sum.inl and FreeMonoid.of ∘ Sum.inr are monoid homomorphisms to the quotient by c.

Defined in

Mathlib.GroupTheory.Coprod.Basic

Cited by

3 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Quot.sound

Assumes

MulOneClassMulOneClass