Mathlib v3 is deprecated. Go to Mathlib v4

Def add_monoid_algebra_equiv_direct_sum

Modification history

2021-05-07 09:30

src/algebra/monoid_algebra_to_direct_sum.lean

feat(algebra/monoid_algebra): add add_monoid_algebra_ring_equiv_direct_sum (#7422) …

Added add_monoid_algebra_equiv_direct_sum View on Github →