English
Right-hand compatibility of scalar actions with the intermediate field, giving SMulCommClass on the right.
Русский
Право-совместимость действий скаляров с промежуточным полем, образующая SMulCommClass справа.
LaTeX
$$$\\text{SMulCommClass } X F Y$ for $F = S$ (as a subfield)$$
Lean4
instance smulCommClass_right [SMul X Y] [SMul L Y] [SMulCommClass X L Y] (F : IntermediateField K L) :
SMulCommClass X F Y :=
inferInstanceAs
(SMulCommClass X F.toSubfield Y)
-- note: giving this instance the default priority may trigger trouble with synthesizing instances
-- for field extensions with more than one intermediate field. For example, in a field extension
-- `E/F`, and with `K₁ ≤ K₂` of type `IntermediateField F E`, this instance will cause a search
-- for `IsScalarTower K₁ K₂ E` to trigger a search for `IsScalarTower E K₂ E` which may
-- take a long time to fail.
