Zulip Chat Archive
Stream: general
Topic: linear_map vs distrib_mul_action_hom
Eric Wieser (Nov 03 2020 at 15:40):
docs#linear_map and docs#distrib_mul_action_hom look isomorphic to me (once you consider docs#linear_map.map_zero) - should one be removed?
Mario Carneiro (Nov 03 2020 at 15:42):
Last updated: May 02 2025 at 03:31 UTC