Documentation

Mathlib.Algebra.Ring.Action.Invariant

Subrings invariant under an action #

class IsInvariantSubring (M : Type u_1) {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (S : Subring R) :

A typeclass for subrings invariant under a MulSemiringAction.

Instances
    def IsInvariantSubring.subtypeHom (M : Type u_1) [Monoid M] {R' : Type u_2} [Ring R'] [MulSemiringAction M R'] (U : Subring R') [IsInvariantSubring M U] :

    The canonical inclusion from an invariant subring.

    Equations
    Instances For
      @[simp]
      @[simp]