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
🔸 coverage
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
      source
      📐 coverage
      @[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) :
      (toRingEquiv G R x).symm a✝ = x⁻¹ • a✝
      source
      📐 coverage
      @[simp]
      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✝