Theorems · Definition · ring theory

FixedPoints.subring

(B : Type u_2) → [inst : Ring B] → (G : Type u_4) → [inst_1 : Monoid G] → [MulSemiringAction G B] → Subring B

The set of fixed points under a group action, as a subring.

Defined in

Mathlib.Algebra.Algebra.Subalgebra.Operations

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

RingMonoidMulSemiringAction