Invariant subrings under restricted actions

An invariant subring for a group action remains invariant after restricting the action to a subgroup. This instance lets constructions such as ramification groups be applied directly to a subgroup of the acting group.

instance Subgroup.isInvariantSubring {G : Type u_1} {R : Type u_2} [Group G] [Ring R] [MulSemiringAction G R] (H : Subgroup G) (S : Subring R) [IsInvariantSubring G S] : IsInvariantSubring (↥H) S

A subring invariant under a group action is invariant under the restricted action of every subgroup.