Theorems · Definition · ring theory

FixedPoints.subsemiring

(B' : Type u_3) →
  [inst : Semiring B'] → (G : Type u_4) → [inst_1 : Monoid G] → [MulSemiringAction G B'] → Subsemiring B'

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

Defined in

Mathlib.Algebra.Algebra.Subalgebra.Operations

Cited by

3 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

SemiringMonoidMulSemiringAction