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.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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✝

@[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✝

@[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.

@[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.

@[implicit_reducible]

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

Equations

• instMulSemiringActionRingEquiv R = { smul := fun (x1 : R ≃+* R) (x2 : R) => x1 x2, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, smul_one := ⋯, smul_mul := ⋯ }