Def Monoid.Coprod.MulEquiv.coprodComm

Modification history

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