instIsInvariantSubfieldSubfield — Mathlib

English

A fixed-by subfield is closed under the field operations and stable under the monoid action.

Русский

Пусть фиксированные элементы образуют подполе, которое замкнуто относительно операций поля и устойчиво при действии моноида.

LaTeX

$$$ \\text{IsInvariantSubfield } M S \\Rightarrow S \\text{ is a subfield stable under M} $$$

Lean4

instance : IsInvariantSubfield M (FixedPoints.subfield M F) where smul_mem g x hx g' := by rw [hx, hx]

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