Zulip Chat Archive
Stream: Is there code for X?
Topic: finsupp equiv dfinsupp
Eric Wieser (Apr 20 2021 at 21:58):
Do we have (ι →₀ M) ≃ (Π₀ i : ι, M) anywhere? Or a special case where the LHS is (add_)monoid_algebra / polynomial / mv_polynomial, and/or the RHS is direct_sum?
Eric Wieser (Apr 20 2021 at 23:20):
Ah, found it: docs#finsupp_lequiv_direct_sum, which is more bundled
Last updated: May 02 2025 at 03:31 UTC