instSMulOfIsScalarTower — Mathlib

English

If S acts on k by a distributive scalar action and there is a compatible scalar tower, then S acts on AlgebraicClosure(k).

Русский

Если S действует на k по распределённому действию скалярами и существует совместимая башня скаляров, то S действует на AlgebraicClosure(k).

LaTeX

$$$ SMul\; S\;\big(\text{AlgebraicClosure}(k)\big) $$$

Lean4

instance {S : Type*} [DistribSMul S k] [IsScalarTower S k k] : SMul S (AlgebraicClosure k) :=
  Submodule.Quotient.instSMul' _

Похожие утверждения