toIsOrderedRing — Mathlib

English

The fixed-point set under a group action on an algebra forms a subalgebra of the ambient algebra.

Русский

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

LaTeX

$$$$\\text{FixedPoints}_G(B) \\text{ is a subalgebra of } B.$$$$

Lean4

instance toIsOrderedRing [CommSemiring R] [Semiring A] [PartialOrder A] [IsOrderedRing A] [Algebra R A]
    (S : Subalgebra R A) : IsOrderedRing S :=
  S.toSubsemiring.toIsOrderedRing

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