subfield — Mathlib

English

The fixed-by subfield of F with respect to an action by M is the subfield consisting of elements fixed by all m ∈ M.

Русский

Подполе фиксированности относительно действия M состоит из элементов, фиксированных для всех m ∈ M.

LaTeX

$$$ \\mathrm{FixedBy.subfield} F M := \\{ x \\in F : m \\cdot x = x \\text{ для всех } m \\in M \\} $$$$

Lean4

/-- The subfield of fixed points by a monoid action. -/
def subfield : Subfield F :=
  Subfield.copy (⨅ m : M, FixedBy.subfield F m) (fixedPoints M F) (by ext; simp [FixedBy.subfield])

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