Zulip Chat Archive
Stream: Is there code for X?
Topic: (R →ₗ[R] M) ≃ M
Chris Hughes (Feb 14 2022 at 11:25):
Do we have something like the universal property of R as an R module?
Eric Wieser (Feb 14 2022 at 11:27):
Perhaps as a linear_equiv?
Eric Wieser (Feb 14 2022 at 11:28):
I think this will be near docs#linear_map.to_span_singleton
Eric Wieser (Feb 14 2022 at 12:28):
docs#linear_map.ring_lmap_equiv_self, found by searching for R →ₗ[R] M
Last updated: May 02 2025 at 03:31 UTC