Structures · Algebra
IsCentralScalar
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
- Shape
- 2 explicit arguments · adds op_smul_eq_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by131
- IsCentralScalar.op_smul_eq_smul
- TrivSqZeroExt.map
- ExteriorAlgebra.toTrivSqZeroExt
- TrivSqZeroExt.map_inr
- TrivSqZeroExt.liftEquivOfComm_apply
- ExteriorAlgebra.toTrivSqZeroExt_ι
- TrivSqZeroExt.kerIdeal
- TrivSqZeroExt.exp_def
- TrivSqZeroExt.liftEquivOfComm
- IsCentralScalar.unop_smul_eq_smul
- TrivSqZeroExt.algHom_ext
- TensorAlgebra.toTrivSqZeroExt
- TrivSqZeroExt.eq_smul_exp_of_invertible
- TrivSqZeroExt.snd_map
- TrivSqZeroExt.map_inl
- TrivSqZeroExt.sndHom_comp_map
- TensorAlgebra.toTrivSqZeroExt_ι
- ExteriorAlgebra.toTrivSqZeroExt_comp_map
- TrivSqZeroExt.algebraMap_eq_inl
- TrivSqZeroExt.fst_map
- TrivSqZeroExt.commRing
- TrivSqZeroExt.algebraMap_eq_inlHom
- ULift.instIsCentralScalar
- TensorProduct.instIsCentralScalar
- TrivSqZeroExt.algebraBase
- AddMonoidAlgebra.isCentralScalar
- TrivSqZeroExt.snd_exp
- Subsemiring.pointwise_central_scalar
- TrivSqZeroExt.map_comp_inrHom
- LieSubmodule.Quotient.isCentralScalar
- lp.instIsCentralScalarPreLp
- IsScalarTower.op_right
- CStarMatrix.instIsCentralScalar
- MeasureTheory.OuterMeasure.instIsCentralScalar
- TrivSqZeroExt.mem_kerIdeal_iff_inr
- IsBoundedSMul.op
- TrivSqZeroExt.snd_pow
- TrivSqZeroExt.map_comp_inlAlgHom
- SubMulAction.isCentralScalar
- Matrix.isCentralScalar
- IsCentralScalar.isLinearTopology_iff
- MonoidAlgebra.isCentralScalar
- CentroidHom.instIsCentralScalar
- TrivSqZeroExt.map_id
- Finsupp.isCentralScalar
- AddSubgroup.pointwise_isCentralScalar
- TrivSqZeroExt.instAlgebra
- TrivSqZeroExt.fst_exp
- Filter.isCentralScalar
- ZeroHom.instIsCentralScalar
Ancestors0
No ancestors.