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
- MulSemiringAction.toRingEquiv G R x = { toEquiv := (DistribMulAction.toAddEquiv R x).toEquiv, map_mul' := ⋯, map_add' := ⋯ }