Mathlib v3 is deprecated. Go to Mathlib v4

Theorem direct_sum.to_add_monoid_algebra_add

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 direct_sum.to_add_monoid_algebra_addView on Github →