doc-next-gen

Mathlib.Algebra.Ring.Action.Group

Module docstring

{"# 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 to avoid needing the import of Mathlib.Algebra.GroupWithZero.Action.Basic. "}

MulSemiringAction.toRingEquiv definition
[MulSemiringAction G R] (x : G) : R ≃+* R
Full source 
/-- Each element of the group defines a semiring isomorphism. -/
@[simps!]
def MulSemiringAction.toRingEquiv [MulSemiringAction G R] (x : G) : R ≃+* R :=
  { DistribMulAction.toAddEquiv R x, MulSemiringAction.toRingHom G R x with }
Ring automorphism induced by group action on a semiring
Informal description
For a group \( G \) acting multiplicatively on a semiring \( R \), each element \( x \in G \) defines a ring automorphism \( R \simeq R \). This automorphism preserves both the additive and multiplicative structures of \( R \).