Zulip Chat Archive
Stream: mathlib4
Topic: StarModule for RCLike
Alex Meiburg (Apr 11 2025 at 16:33):
I was a bit surprised that RCLike k doesn't give a StarModule Real k. It's easy to write one, as far as I can tell, this only adds a prop (and not any potentially weird definitions). Is there a reason this instance doesn't exist, or should I PR it?
Jireh Loreaux (Apr 11 2025 at 18:19):
Sure, that should be fine to add.
Alex Meiburg (Apr 11 2025 at 19:21):
Cool! #23960
Kevin Buzzard (Apr 12 2025 at 07:22):
Kevin Buzzard (Apr 12 2025 at 07:23):
This instance could also be made for the nonexisting Prop-valued IsROrC.
Last updated: May 02 2025 at 03:31 UTC