Commit 2025-06-17 09:45 260a5983

View on Github →

chore(GroupTheory/Coprod/Basic): use to_additive (#25998) This PR add a use of to_additive. It also fixes a namespace problem. As written in the doc-comment of the file, we can see that the old namespacing was wrong. (and this caused the name to not properly additivise)

Estimated changes

Modified Mathlib/GroupTheory/Coprod/Basic.lean

deleted def Monoid.AddEquiv.coprodUnit

deleted def Monoid.AddEquiv.punitCoprod

added def Monoid.Coprod.MulEquiv.coprodAssoc

added theorem Monoid.Coprod.MulEquiv.coprodAssoc_apply_inl_inl

added theorem Monoid.Coprod.MulEquiv.coprodAssoc_apply_inl_inr

added theorem Monoid.Coprod.MulEquiv.coprodAssoc_apply_inr

added theorem Monoid.Coprod.MulEquiv.coprodAssoc_symm_apply_inl

added theorem Monoid.Coprod.MulEquiv.coprodAssoc_symm_apply_inr_inl

added theorem Monoid.Coprod.MulEquiv.coprodAssoc_symm_apply_inr_inr

added def Monoid.Coprod.MulEquiv.coprodComm

added def Monoid.Coprod.MulEquiv.coprodCongr

added def Monoid.Coprod.MulEquiv.coprodPUnit

added def Monoid.Coprod.MulEquiv.punitCoprod

deleted def Monoid.MulEquiv.coprodAssoc

deleted theorem Monoid.MulEquiv.coprodAssoc_apply_inl_inl

deleted theorem Monoid.MulEquiv.coprodAssoc_apply_inl_inr

deleted theorem Monoid.MulEquiv.coprodAssoc_apply_inr

deleted theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inl

deleted theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inr_inl

deleted theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inr_inr

deleted def Monoid.MulEquiv.coprodComm

deleted def Monoid.MulEquiv.coprodCongr

deleted def Monoid.MulEquiv.coprodPUnit

deleted def Monoid.MulEquiv.punitCoprod