mathlib3 documentation

algebra.group_ring_action.invariant

Subrings invariant under an action #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[class]
structure is_invariant_subring (M : Type u_1) {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (S : subring R) :
Prop

A typeclass for subrings invariant under a mul_semiring_action.

Instances of this typeclass
@[protected, instance]
Equations
def is_invariant_subring.subtype_hom (M : Type u_1) [monoid M] {R' : Type u_2} [ring R'] [mul_semiring_action M R'] (U : subring R') [is_invariant_subring M U] :

The canonical inclusion from an invariant subring.

Equations