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

@[simp]
theorem MulSemiringAction.toRingEquiv_apply (G : Type u_1) [Group G] (R : Type u_2) [Semiring R] [MulSemiringAction G R] (x : G) :
∀ (a : R), (MulSemiringAction.toRingEquiv G R x) a = x a
@[simp]
theorem MulSemiringAction.toRingEquiv_symm_apply (G : Type u_1) [Group G] (R : Type u_2) [Semiring R] [MulSemiringAction G R] (x : G) :
∀ (a : R), (MulSemiringAction.toRingEquiv G R x).symm a = x⁻¹ a
def MulSemiringAction.toRingEquiv (G : Type u_1) [Group G] (R : Type u_2) [Semiring R] [MulSemiringAction G R] (x : G) :
R ≃+* R

Each element of the group defines a semiring isomorphism.

Equations
Instances For