Theorems · Inductive type · group theory

IsCentralScalar

(M : Type u_9) → (α : Type u_10) → [SMul M α] → [SMul Mᵐᵒᵖ α] → Prop

A typeclass indicating that the right (aka MulOpposite) and left actions by M on α are equal, that is that M acts centrally on α. This can be thought of as a version of commutativity for •.

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

39 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

SMulSMul