subalgebra — Mathlib

English

The fixed-point set under a group action on a ring forms a subring of that ring.

Русский

Множество фиксированных точек при действии группы на кольцо образует подкольцо этого кольца.

LaTeX

$$$$\\text{FixedPoints}_G(B) \\le B \\quad\\text{and}\\quad \\text{FixedPoints}_G(B) \\text{ is a subring of } B.$$$$

Lean4

/-- The set of fixed points under a group action, as a subalgebra. -/
def subalgebra : Subalgebra A B where
  __ := FixedPoints.addSubgroup G B
  __ := FixedPoints.submonoid G B
  algebraMap_mem' r := by simp

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