Def Monoid.Coprod.MulEquiv.punitCoprod

Modification history

2025-06-17 09:45

Mathlib/GroupTheory/Coprod/Basic.lean

chore(GroupTheory/Coprod/Basic): use `to_additive` (#25998) …

Added Monoid.Coprod.MulEquiv.punitCoprod View on Github →