Def DirectSum.addEquivProd

Modification history

2024-11-05 15:53
Mathlib/Algebra/DirectSum/Basic.lean
multiplicative version of classification of finite abelian groups (#18659) …
Added DirectSum.addEquivProdView on Github →