Theorems · Theorem · ring theory

MulSemiringAction.toRingEquiv_apply_symm_apply

∀ (G : Type u_1) [inst : Group G] (R : Type u_2) [inst_1 : Semiring R] [inst_2 : MulSemiringAction G R] (x : G) (a : R),
  ((MulSemiringAction.toRingEquiv G R) x).symm a = x⁻¹ • a

Defined in

Mathlib.Algebra.Ring.Action.Group

Cited by

4 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupSemiringMulSemiringAction