Theorem Monoid.Coprod.MulEquiv.coprodAssoc_apply_inl_inr

Modification history

2025-06-17 09:45
Mathlib/GroupTheory/Coprod/Basic.lean
chore(GroupTheory/Coprod/Basic): use `to_additive` (#25998) …
Added Monoid.Coprod.MulEquiv.coprodAssoc_apply_inl_inrView on Github →