Zulip Chat Archive
Stream: maths
Topic: is_ring_hom left multiplication
Casper Putz (Jan 24 2019 at 10:07):
Is the statement that left (or right) mulitiplication by an element of a ring is a ring homomorphism in mathlib?
Neil Strickland (Jan 24 2019 at 10:08):
I hope not. Presumably you mean "linear map" rather than "ring homomorphism"?
Casper Putz (Jan 24 2019 at 10:36):
Oh you're right. durp... It is a linear map so I should use that. Thanks
Last updated: Dec 20 2023 at 11:08 UTC