Commit 2023-09-04 17:05 22f1f9fc

View on Github →

feat: Binary coproducts of Monoids (#6828)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Coprod.lean

added inductive Monoid.Coprod.Rel

added theorem Monoid.Coprod.ext_hom

added theorem Monoid.Coprod.induction_on

added def Monoid.Coprod.inl

added theorem Monoid.Coprod.inl_apply

added theorem Monoid.Coprod.inl_injective

added theorem Monoid.Coprod.inl_leftInverse

added def Monoid.Coprod.inr

added theorem Monoid.Coprod.inr_apply

added theorem Monoid.Coprod.inr_injective

added theorem Monoid.Coprod.inr_leftInverse

added theorem Monoid.Coprod.inv_def

added def Monoid.Coprod.lift

added theorem Monoid.Coprod.lift_inl

added theorem Monoid.Coprod.lift_inr

added theorem Monoid.Coprod.lift_mrange_le

added theorem Monoid.Coprod.lift_range_le

added theorem Monoid.Coprod.mrange_eq_sup

added theorem Monoid.Coprod.range_eq_sup

added def Monoid.Coprod