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]
def
is_invariant_subring.to_mul_semiring_action
(M : Type u_1)
{R : Type u_2}
[monoid M]
[ring R]
[mul_semiring_action M R]
(S : subring R)
[is_invariant_subring M S] :
Equations
- is_invariant_subring.to_mul_semiring_action M S = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := λ (m : M) (x : ↥S), ⟨m • ↑x, _⟩}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}
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.
@[simp]
theorem
is_invariant_subring.coe_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] :
@[simp]
theorem
is_invariant_subring.coe_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] :