Theorems · Definition · group theory

AddMonoid.coprodCon

(M : Type u_1) → (N : Type u_2) → [AddZeroClass M] → [AddZeroClass N] → AddCon (FreeAddMonoid (M ⊕ N))

The minimal additive congruence relation c on FreeAddMonoid (M ⊕ N) such that FreeAddMonoid.of ∘ Sum.inl and FreeAddMonoid.of ∘ Sum.inr are additive 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

AddZeroClassAddZeroClass