Documentation

Mathlib.Algebra.Ring.Action.Group

If a group acts multiplicatively on a semiring, each group element acts by a ring automorphism. #

This result is split out from Mathlib/Algebra/Ring/Action/Basic.lean to avoid needing the import of Mathlib/Algebra/GroupWithZero/Action/Basic.lean.

source
def MulSemiringAction.toRingEquiv (G : Type u_1) [Group G] (R : Type u_2) [Semiring R] [MulSemiringAction G R] :
G →* R ≃+* R

Each element of the group defines a semiring isomorphism.

Instances For
    source
    @[simp]
    theorem MulSemiringAction.toRingEquiv_apply_apply (G : Type u_1) [Group G] (R : Type u_2) [Semiring R] [MulSemiringAction G R] (x : G) (a✝ : R) :
    ((toRingEquiv G R) x) a✝ = x • a✝
    source
    @[simp]
    theorem MulSemiringAction.toRingEquiv_apply_symm_apply (G : Type u_1) [Group G] (R : Type u_2) [Semiring R] [MulSemiringAction G R] (x : G) (a✝ : R) :
    ((toRingEquiv G R) x).symm a✝ = x⁻¹ • a✝
    source
    @[deprecated MulSemiringAction.toRingEquiv_apply_apply (since := "2026-06-19")]
    theorem MulSemiringAction.toRingEquiv_apply (G : Type u_1) [Group G] (R : Type u_2) [Semiring R] [MulSemiringAction G R] (x : G) (a✝ : R) :
    ((toRingEquiv G R) x) a✝ = x • a✝

    Alias of MulSemiringAction.toRingEquiv_apply_apply.

    source
    @[deprecated MulSemiringAction.toRingEquiv_apply_symm_apply (since := "2026-06-19")]
    theorem MulSemiringAction.toRingEquiv_symm_apply (G : Type u_1) [Group G] (R : Type u_2) [Semiring R] [MulSemiringAction G R] (x : G) (a✝ : R) :
    ((toRingEquiv G R) x).symm a✝ = x⁻¹ • a✝

    Alias of MulSemiringAction.toRingEquiv_apply_symm_apply.

    source
    @[instance_reducible]
    instance instMulSemiringActionRingEquiv (R : Type u_2) [Semiring R] :
    MulSemiringAction (R ≃+* R) R