THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
These are defined in this file as
semirings are not available yet where
subring are provided next to the other scalar actions instances
for those subobjects.