Theorems · Theorem · ring theory

MulSemiringAction.toRingEquiv_symm_apply

Deprecated since 2026-06-19Use MulSemiringAction.toRingEquiv_apply_symm_apply instead.

∀ (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

Alias of MulSemiringAction.toRingEquiv_apply_symm_apply.

Defined in

Mathlib.Algebra.Ring.Action.Group

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupSemiringMulSemiringAction