Commit 2023-09-15 18:54 6d72cf86

View on Github →

refactor: redefine Monoid.Coprod (#2214)

Redefine Monoid.Coprod.
Use @[to_additive].
Expand API.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Congruence.lean

added theorem Con.map_of_mul_left_rel_one

Deleted Mathlib/GroupTheory/Coprod.lean

deleted inductive Monoid.Coprod.Rel

deleted theorem Monoid.Coprod.ext_hom

deleted theorem Monoid.Coprod.induction_on

deleted def Monoid.Coprod.inl

deleted theorem Monoid.Coprod.inl_apply

deleted theorem Monoid.Coprod.inl_injective

deleted theorem Monoid.Coprod.inl_leftInverse

deleted def Monoid.Coprod.inr

deleted theorem Monoid.Coprod.inr_apply

deleted theorem Monoid.Coprod.inr_injective

deleted theorem Monoid.Coprod.inr_leftInverse

deleted theorem Monoid.Coprod.inv_def

deleted def Monoid.Coprod.lift

deleted theorem Monoid.Coprod.lift_inl

deleted theorem Monoid.Coprod.lift_inr

deleted theorem Monoid.Coprod.lift_mrange_le

deleted theorem Monoid.Coprod.lift_range_le

deleted theorem Monoid.Coprod.mrange_eq_sup

deleted theorem Monoid.Coprod.range_eq_sup

deleted def Monoid.Coprod

Created Mathlib/GroupTheory/Coprod/Basic.lean

added def Monoid.AddEquiv.coprodUnit

added def Monoid.AddEquiv.punitCoprod

added def Monoid.Coprod.clift

added theorem Monoid.Coprod.clift_apply_inl

added theorem Monoid.Coprod.clift_apply_inr

added theorem Monoid.Coprod.clift_apply_mk

added theorem Monoid.Coprod.clift_comp_mk

added theorem Monoid.Coprod.clift_mk

added theorem Monoid.Coprod.closure_range_inl_union_inr

added theorem Monoid.Coprod.codisjoint_mrange_inl_mrange_inr

added theorem Monoid.Coprod.codisjoint_range_inl_range_inr

added theorem Monoid.Coprod.comp_lift

added theorem Monoid.Coprod.con_ker_mk

added theorem Monoid.Coprod.con_mul_left_inv

added def Monoid.Coprod.fst

added theorem Monoid.Coprod.fst_apply_inl

added theorem Monoid.Coprod.fst_apply_inr

added theorem Monoid.Coprod.fst_comp_inl

added theorem Monoid.Coprod.fst_comp_inr

added theorem Monoid.Coprod.fst_comp_swap

added theorem Monoid.Coprod.fst_comp_toProd

added theorem Monoid.Coprod.fst_prod_snd

added theorem Monoid.Coprod.fst_surjective

added theorem Monoid.Coprod.fst_swap

added theorem Monoid.Coprod.fst_toProd

added theorem Monoid.Coprod.hom_ext

added theorem Monoid.Coprod.induction_on'

added theorem Monoid.Coprod.induction_on

added def Monoid.Coprod.inl

added theorem Monoid.Coprod.inl_injective

added def Monoid.Coprod.inr

added theorem Monoid.Coprod.inr_injective

added theorem Monoid.Coprod.inv_def

added def Monoid.Coprod.lift

added def Monoid.Coprod.liftEquiv

added theorem Monoid.Coprod.lift_apply_inl

added theorem Monoid.Coprod.lift_apply_inr

added theorem Monoid.Coprod.lift_apply_mk

added theorem Monoid.Coprod.lift_comp_inl

added theorem Monoid.Coprod.lift_comp_inr

added theorem Monoid.Coprod.lift_comp_swap

added theorem Monoid.Coprod.lift_inl_inr

added theorem Monoid.Coprod.lift_inr_inl

added theorem Monoid.Coprod.lift_swap

added theorem Monoid.Coprod.lift_unique

added def Monoid.Coprod.map

added theorem Monoid.Coprod.map_apply_inl

added theorem Monoid.Coprod.map_apply_inr

added theorem Monoid.Coprod.map_comp_inl

added theorem Monoid.Coprod.map_comp_inr

added theorem Monoid.Coprod.map_comp_map

added theorem Monoid.Coprod.map_id_id

added theorem Monoid.Coprod.map_map

added theorem Monoid.Coprod.map_mk_ofList

added theorem Monoid.Coprod.mclosure_range_inl_union_inr

added def Monoid.Coprod.mk

added theorem Monoid.Coprod.mk_eq_mk

added theorem Monoid.Coprod.mk_of_inl

added theorem Monoid.Coprod.mk_of_inr

added theorem Monoid.Coprod.mk_of_inv_mul

added theorem Monoid.Coprod.mk_surjective

added theorem Monoid.Coprod.mker_swap

added theorem Monoid.Coprod.mrange_eq

added theorem Monoid.Coprod.mrange_inl_sup_mrange_inr

added theorem Monoid.Coprod.mrange_lift

added theorem Monoid.Coprod.mrange_mk

added theorem Monoid.Coprod.mrange_swap

added theorem Monoid.Coprod.prod_mk_fst_snd

added theorem Monoid.Coprod.range_eq

added theorem Monoid.Coprod.range_inl_sup_range_inr

added theorem Monoid.Coprod.range_lift

added theorem Monoid.Coprod.range_swap

added def Monoid.Coprod.snd

added theorem Monoid.Coprod.snd_apply_inl

added theorem Monoid.Coprod.snd_apply_inr

added theorem Monoid.Coprod.snd_comp_inl

added theorem Monoid.Coprod.snd_comp_inr

added theorem Monoid.Coprod.snd_comp_swap

added theorem Monoid.Coprod.snd_comp_toProd

added theorem Monoid.Coprod.snd_surjective

added theorem Monoid.Coprod.snd_swap

added theorem Monoid.Coprod.snd_toProd

added def Monoid.Coprod.swap

added theorem Monoid.Coprod.swap_bijective

added theorem Monoid.Coprod.swap_comp_inl

added theorem Monoid.Coprod.swap_comp_inr

added theorem Monoid.Coprod.swap_comp_map

added theorem Monoid.Coprod.swap_comp_swap

added theorem Monoid.Coprod.swap_eq_one

added theorem Monoid.Coprod.swap_inj

added theorem Monoid.Coprod.swap_injective

added theorem Monoid.Coprod.swap_inl

added theorem Monoid.Coprod.swap_inr

added theorem Monoid.Coprod.swap_map

added theorem Monoid.Coprod.swap_surjective

added theorem Monoid.Coprod.swap_swap

added def Monoid.Coprod.toProd

added theorem Monoid.Coprod.toProd_apply_inl

added theorem Monoid.Coprod.toProd_apply_inr

added theorem Monoid.Coprod.toProd_comp_inl

added theorem Monoid.Coprod.toProd_comp_inr

added theorem Monoid.Coprod.toProd_surjective

added def Monoid.Coprod

added def Monoid.MulEquiv.coprodAssoc

added theorem Monoid.MulEquiv.coprodAssoc_apply_inl_inl

added theorem Monoid.MulEquiv.coprodAssoc_apply_inl_inr

added theorem Monoid.MulEquiv.coprodAssoc_apply_inr

added theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inl

added theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inr_inl

added theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inr_inr

added def Monoid.MulEquiv.coprodComm

added def Monoid.MulEquiv.coprodCongr

added def Monoid.MulEquiv.coprodPUnit

added def Monoid.MulEquiv.punitCoprod

added def Monoid.coprodCon

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean