Theorem MonoidHom.noncommPiCoprod_mrange

Modification history

2023-02-23 03:04
Mathlib/GroupTheory/NoncommPiCoprod.lean
feat: port GroupTheory.NoncommPiCoprod (#2449)
Added MonoidHom.noncommPiCoprod_mrangeView on Github →