Mathlib v3 is deprecated. Go to Mathlib v4

Def Module.biprod_iso_prod

Modification history

2022-05-08 06:24

src/algebra/category/Module/biproducts.lean

feat(algebra/category/Module): biproducts (#13908) …

Added Module.biprod_iso_prod View on Github →