Theorem Monoid.Coprod.MulEquiv.coprodAssoc_symm_apply_inr_inl

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_symm_apply_inr_inlView on Github →