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: May 02 2025 at 03:31 UTC