Mathlib v3 is deprecated. Go to Mathlib v4

Def direct_sum.from_add_monoid

Modification history

2020-12-14 13:16

src/algebra/direct_sum.lean

feat(algebra/direct_sum): constructor for morphisms into direct sums (#5204)

Added direct_sum.from_add_monoid View on Github →