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):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/new.20definition.20of.20linear_map

Last updated: Dec 20 2023 at 11:08 UTC