instIsInvariantSubringOfIsInvariantSubfield

English

If S is an invariant subfield under M-action, then S.toSubring is an invariant subring under M-action.

Русский

Если S инвариантно относительно действия M, то S.toSubring также инвариантно относительно M.

LaTeX

$$$ [IsInvariantSubfield\\ M\\ S] \\Rightarrow IsInvariantSubring M S.toSubring $$$

Lean4

instance [IsInvariantSubfield M S] : IsInvariantSubring M S.toSubring where smul_mem := IsInvariantSubfield.smul_mem

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