Def Monoid.Coprod.MulEquiv.coprodPUnit

Modification history

2025-06-17 09:45

Mathlib/GroupTheory/Coprod/Basic.lean

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

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